Mathlib.Topology.MetricSpace.DilationEquiv

DilationEquivClass structure

[EquivLike F X Y]

Full source

/-- Typeclass saying that `F` is a type of bundled equivalences such that all `e : F` are
dilations. -/
class DilationEquivClass [EquivLike F X Y] : Prop where
  edist_eq' : ∀ f : F, ∃ r : ℝ≥0, r ≠ 0 ∧ ∀ x y : X, edist (f x) (f y) = r * edist x y

Dilation Equivalence Class

Informal description

The class `DilationEquivClass F X Y` expresses that terms of type `F` can be injectively coerced to bijective dilation maps between pseudo-emetric spaces `X` and `Y`. A dilation map is a function that scales distances by a fixed positive real factor, i.e., there exists $r > 0$ such that for all $x, y \in X$, the distance between $f(x)$ and $f(y)$ in $Y$ is $r$ times the distance between $x$ and $y$ in $X$.

instDilationClassOfDilationEquivClass instance

[EquivLike F X Y] [DilationEquivClass F X Y] : DilationClass F X Y

Full source

instance (priority := 100) [EquivLike F X Y] [DilationEquivClass F X Y] : DilationClass F X Y :=
  { inferInstanceAs (FunLike F X Y), ‹DilationEquivClass F X Y› with }

Dilation Equivalence Class as Dilation Class

Informal description

For any type `F` that is an instance of `EquivLike` and `DilationEquivClass` between pseudo-emetric spaces `X` and `Y`, there is a canonical `DilationClass` instance that allows elements of `F` to be treated as dilation maps from `X` to `Y`. A dilation map is a function that scales distances by a fixed positive real factor, i.e., there exists $r > 0$ such that for all $x, y \in X$, the distance between $f(x)$ and $f(y)$ in $Y$ is $r$ times the distance between $x$ and $y$ in $X$.

DilationEquiv structure

(X Y : Type*) [PseudoEMetricSpace X] [PseudoEMetricSpace Y]
    extends X ≃ Y, Dilation X Y

Full source

/-- Type of equivalences `X ≃ Y` such that `∀ x y, edist (f x) (f y) = r * edist x y` for some
`r : ℝ≥0`, `r ≠ 0`. -/
structure DilationEquiv (X Y : Type*) [PseudoEMetricSpace X] [PseudoEMetricSpace Y]
    extends X ≃ Y, Dilation X Y

Dilation Equivalence between Pseudo-EMetric Spaces

Informal description

A `DilationEquiv X Y` is a type of bundled equivalences between pseudo-emetric spaces `X` and `Y` such that there exists a positive real number `r` satisfying the dilation property: for all `x, y ∈ X`, the emetric distance between the images `f(x)` and `f(y)` equals `r` times the emetric distance between `x` and `y`. This structure extends both the notion of an equivalence (`X ≃ Y`) and a dilation map (`Dilation X Y`), combining the bijective property of equivalences with the distance-scaling property of dilations.

term_≃ᵈ_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc] infixl:25 " ≃ᵈ " => DilationEquiv

Dilation equivalence notation

Informal description

The notation `≃ᵈ` represents dilation equivalences between two pseudo-emetric spaces `X` and `Y`. A dilation equivalence is a bundled equivalence `f : X ≃ Y` such that there exists a positive real number `r` satisfying the condition that the emetric distance between `f x` and `f y` is equal to `r` times the emetric distance between `x` and `y` for all `x, y ∈ X`.

DilationEquiv.instEquivLike instance

: EquivLike (X ≃ᵈ Y) X Y

Full source

instance : EquivLike (X ≃ᵈ Y) X Y where
  coe f := f.1
  inv f := f.1.symm
  left_inv f := f.left_inv'
  right_inv f := f.right_inv'
  coe_injective' := by rintro ⟨⟩ ⟨⟩ h -; congr; exact DFunLike.ext' h

Dilation Equivalence as Function-Like Object

Informal description

For any two pseudo-emetric spaces $X$ and $Y$, a dilation equivalence $X \simeq^d Y$ can be treated as a function-like object from $X$ to $Y$ that preserves the equivalence structure.

DilationEquiv.instDilationEquivClass instance

: DilationEquivClass (X ≃ᵈ Y) X Y

Full source

instance : DilationEquivClass (X ≃ᵈ Y) X Y where
  edist_eq' f := f.edist_eq'

Dilation Equivalence Class for Pseudo-EMetric Spaces

Informal description

For any two pseudo-emetric spaces $X$ and $Y$, the type of dilation equivalences $X \simeq^d Y$ forms a class of dilation equivalence maps, where each equivalence $e$ satisfies the property that there exists a positive real number $r$ such that for all $x, y \in X$, the emetric distance between $e(x)$ and $e(y)$ in $Y$ is $r$ times the emetric distance between $x$ and $y$ in $X$.

DilationEquiv.coe_toEquiv theorem

(e : X ≃ᵈ Y) : ⇑e.toEquiv = e

Full source

@[simp] theorem coe_toEquiv (e : X ≃ᵈ Y) : ⇑e.toEquiv = e := rfl

Equality of Dilation Equivalence and its Underlying Equivalence Map

Informal description

For any dilation equivalence $e : X \simeq^d Y$ between pseudo-emetric spaces $X$ and $Y$, the underlying equivalence map $\text{toEquiv}(e)$ is equal to $e$ when viewed as a function.

DilationEquiv.ext theorem

{e e' : X ≃ᵈ Y} (h : ∀ x, e x = e' x) : e = e'

Full source

@[ext]
protected theorem ext {e e' : X ≃ᵈ Y} (h : ∀ x, e x = e' x) : e = e' :=
  DFunLike.ext _ _ h

Extensionality of Dilation Equivalences

Informal description

For any two dilation equivalences $e, e' \colon X \simeq^d Y$ between pseudo-emetric spaces $X$ and $Y$, if $e(x) = e'(x)$ for all $x \in X$, then $e = e'$.

DilationEquiv.symm definition

(e : X ≃ᵈ Y) : Y ≃ᵈ X

Full source

/-- Inverse `DilationEquiv`. -/
def symm (e : X ≃ᵈ Y) : Y ≃ᵈ X where
  toEquiv := e.1.symm
  edist_eq' := by
    refine ⟨(ratio e)⁻¹, inv_ne_zero <| ratio_ne_zero e, e.surjective.forall₂.2 fun x y ↦ ?_⟩
    simp_rw [Equiv.toFun_as_coe, Equiv.symm_apply_apply, coe_toEquiv, edist_eq]
    rw [← mul_assoc, ← ENNReal.coe_mul, inv_mul_cancel₀ (ratio_ne_zero e),
      ENNReal.coe_one, one_mul]

Inverse dilation equivalence

Informal description

Given a dilation equivalence $e \colon X \simeq^d Y$ between pseudo-emetric spaces $X$ and $Y$, the inverse dilation equivalence $e^{-1} \colon Y \simeq^d X$ is defined such that for all $x, y \in Y$, the emetric distance satisfies $\text{edist}(e^{-1}(x), e^{-1}(y)) = r^{-1} \cdot \text{edist}(x, y)$, where $r$ is the dilation ratio of $e$.

DilationEquiv.symm_symm theorem

(e : X ≃ᵈ Y) : e.symm.symm = e

Full source

@[simp] theorem symm_symm (e : X ≃ᵈ Y) : e.symm.symm = e := rfl

Double Inverse Property of Dilation Equivalences

Informal description

For any dilation equivalence $e \colon X \simeq^d Y$ between pseudo-emetric spaces $X$ and $Y$, the double inverse $e^{-1^{-1}}$ equals $e$ itself, i.e., $(e^{-1})^{-1} = e$.

DilationEquiv.symm_bijective theorem

: Function.Bijective (DilationEquiv.symm : (X ≃ᵈ Y) → Y ≃ᵈ X)

Full source

theorem symm_bijective : Function.Bijective (DilationEquiv.symm : (X ≃ᵈ Y) → Y ≃ᵈ X) :=
  Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩

Bijectivity of the Inverse Operation on Dilation Equivalences

Informal description

The function that maps a dilation equivalence $e \colon X \simeq^d Y$ between pseudo-emetric spaces $X$ and $Y$ to its inverse $e^{-1} \colon Y \simeq^d X$ is bijective. That is, the inverse operation is both injective and surjective on the set of dilation equivalences.

DilationEquiv.apply_symm_apply theorem

(e : X ≃ᵈ Y) (x : Y) : e (e.symm x) = x

Full source

@[simp] theorem apply_symm_apply (e : X ≃ᵈ Y) (x : Y) : e (e.symm x) = x := e.right_inv x

Dilation Equivalence Inverse Application Property

Informal description

For any dilation equivalence $e \colon X \simeq^d Y$ between pseudo-emetric spaces $X$ and $Y$, and for any point $x \in Y$, applying $e$ to the inverse image $e^{-1}(x)$ yields $x$, i.e., $e(e^{-1}(x)) = x$.

DilationEquiv.symm_apply_apply theorem

(e : X ≃ᵈ Y) (x : X) : e.symm (e x) = x

Full source

@[simp] theorem symm_apply_apply (e : X ≃ᵈ Y) (x : X) : e.symm (e x) = x := e.left_inv x

Inverse Dilation Equivalence Property: $e^{-1}(e(x)) = x$

Informal description

For any dilation equivalence $e \colon X \simeq^d Y$ between pseudo-emetric spaces $X$ and $Y$, and for any point $x \in X$, applying the inverse dilation equivalence $e^{-1}$ to the image $e(x)$ recovers the original point $x$, i.e., $e^{-1}(e(x)) = x$.

DilationEquiv.Simps.symm_apply definition

(e : X ≃ᵈ Y) : Y → X

Full source

/-- See Note [custom simps projection]. -/
def Simps.symm_apply (e : X ≃ᵈ Y) : Y → X := e.symm

Inverse function of a dilation equivalence

Informal description

The function that maps a point $y \in Y$ to its preimage under the dilation equivalence $e \colon X \simeq^d Y$, i.e., the inverse function $e^{-1}(y) \in X$.

DilationEquiv.ratio_toDilation theorem

(e : X ≃ᵈ Y) : ratio e.toDilation = ratio e

Full source

lemma ratio_toDilation (e : X ≃ᵈ Y) : ratio e.toDilation = ratio e := rfl

Dilation Ratio Preservation under Equivalence-to-Dilation Conversion

Informal description

For any dilation equivalence $e \colon X \simeq^d Y$ between pseudo-emetric spaces $X$ and $Y$, the dilation ratio of the underlying dilation map $e.toDilation$ is equal to the dilation ratio of $e$ itself, i.e., $\text{ratio}(e.toDilation) = \text{ratio}(e)$.

DilationEquiv.refl definition

(X : Type*) [PseudoEMetricSpace X] : X ≃ᵈ X

Full source

/-- Identity map as a `DilationEquiv`. -/
@[simps! -fullyApplied apply]
def refl (X : Type*) [PseudoEMetricSpace X] : X ≃ᵈ X where
  toEquiv := .refl X
  edist_eq' := ⟨1, one_ne_zero, fun _ _ ↦ by simp⟩

Identity dilation equivalence

Informal description

The identity dilation equivalence on a pseudo-emetric space $X$, which is the bijection from $X$ to itself given by the identity function, with the dilation ratio $r = 1$. This means that for any $x, y \in X$, the emetric distance between $x$ and $y$ is preserved under this equivalence.

DilationEquiv.refl_symm theorem

: (refl X).symm = refl X

Full source

@[simp] theorem refl_symm : (refl X).symm = refl X := rfl

Inverse of Identity Dilation Equivalence is Identity

Informal description

The inverse of the identity dilation equivalence on a pseudo-emetric space $X$ is equal to the identity dilation equivalence itself, i.e., $(\text{refl } X)^{-1} = \text{refl } X$.

DilationEquiv.ratio_refl theorem

: ratio (refl X) = 1

Full source

@[simp] theorem ratio_refl : ratio (refl X) = 1 := Dilation.ratio_id

Dilation Ratio of Identity Equivalence is One

Informal description

For any pseudo-emetric space $X$, the dilation ratio of the identity dilation equivalence $\text{refl}_X$ is equal to $1$.

DilationEquiv.trans definition

(e₁ : X ≃ᵈ Y) (e₂ : Y ≃ᵈ Z) : X ≃ᵈ Z

Full source

/-- Composition of `DilationEquiv`s. -/
@[simps! -fullyApplied apply]
def trans (e₁ : X ≃ᵈ Y) (e₂ : Y ≃ᵈ Z) : X ≃ᵈ Z where
  toEquiv := e₁.1.trans e₂.1
  __ := e₂.toDilation.comp e₁.toDilation

Composition of dilation equivalences

Informal description

Given two dilation equivalences $e₁ : X ≃ᵈ Y$ and $e₂ : Y ≃ᵈ Z$, their composition $e₂ ∘ e₁$ forms a dilation equivalence $X ≃ᵈ Z$, where the underlying equivalence is the composition of the underlying equivalences of $e₁$ and $e₂$, and the dilation property is preserved with the ratio being the product of the individual ratios.

DilationEquiv.refl_trans theorem

(e : X ≃ᵈ Y) : (refl X).trans e = e

Full source

@[simp] theorem refl_trans (e : X ≃ᵈ Y) : (refl X).trans e = e := rfl

Identity Dilation Equivalence is Left Identity under Composition

Informal description

For any dilation equivalence $e : X \simeq_{\text{d}} Y$ between pseudo-emetric spaces $X$ and $Y$, the composition of the identity dilation equivalence on $X$ with $e$ is equal to $e$ itself, i.e., $(\text{refl}_X) \circ e = e$.

DilationEquiv.trans_refl theorem

(e : X ≃ᵈ Y) : e.trans (refl Y) = e

Full source

@[simp] theorem trans_refl (e : X ≃ᵈ Y) : e.trans (refl Y) = e := rfl

Right Identity Law for Dilation Equivalence Composition

Informal description

For any dilation equivalence $e : X \simeq_{\text{d}} Y$, the composition of $e$ with the identity dilation equivalence on $Y$ is equal to $e$ itself, i.e., $e \circ \text{id}_Y = e$.

DilationEquiv.symm_trans_self theorem

(e : X ≃ᵈ Y) : e.symm.trans e = refl Y

Full source

@[simp] theorem symm_trans_self (e : X ≃ᵈ Y) : e.symm.trans e = refl Y :=
  DilationEquiv.ext e.apply_symm_apply

Inverse Composition Yields Identity: $e^{-1} \circ e = \text{id}_Y$

Informal description

For any dilation equivalence $e \colon X \simeq^d Y$ between pseudo-emetric spaces $X$ and $Y$, the composition of the inverse equivalence $e^{-1}$ with $e$ is equal to the identity dilation equivalence on $Y$, i.e., $e^{-1} \circ e = \text{id}_Y$.

DilationEquiv.self_trans_symm theorem

(e : X ≃ᵈ Y) : e.trans e.symm = refl X

Full source

@[simp] theorem self_trans_symm (e : X ≃ᵈ Y) : e.trans e.symm = refl X :=
  DilationEquiv.ext e.symm_apply_apply

Composition of Dilation Equivalence with Its Inverse Yields Identity

Informal description

For any dilation equivalence $e \colon X \simeq^d Y$ between pseudo-emetric spaces $X$ and $Y$, the composition of $e$ with its inverse $e^{-1}$ yields the identity dilation equivalence on $X$, i.e., $e \circ e^{-1} = \text{id}_X$.

DilationEquiv.surjective theorem

(e : X ≃ᵈ Y) : Surjective e

Full source

protected theorem surjective (e : X ≃ᵈ Y) : Surjective e := e.1.surjective

Surjectivity of Dilation Equivalences

Informal description

For any dilation equivalence $e : X \simeq^d Y$ between pseudo-emetric spaces $X$ and $Y$, the map $e : X \to Y$ is surjective.

DilationEquiv.bijective theorem

(e : X ≃ᵈ Y) : Bijective e

Full source

protected theorem bijective (e : X ≃ᵈ Y) : Bijective e := e.1.bijective

Bijectivity of Dilation Equivalences

Informal description

For any dilation equivalence $e : X \simeq^d Y$ between pseudo-emetric spaces $X$ and $Y$, the map $e : X \to Y$ is bijective.

DilationEquiv.injective theorem

(e : X ≃ᵈ Y) : Injective e

Full source

protected theorem injective (e : X ≃ᵈ Y) : Injective e := e.1.injective

Injectivity of Dilation Equivalences

Informal description

For any dilation equivalence $e : X \simeq^d Y$ between pseudo-emetric spaces $X$ and $Y$, the map $e : X \to Y$ is injective.

DilationEquiv.ratio_trans theorem

(e : X ≃ᵈ Y) (e' : Y ≃ᵈ Z) : ratio (e.trans e') = ratio e * ratio e'

Full source

@[simp]
theorem ratio_trans (e : X ≃ᵈ Y) (e' : Y ≃ᵈ Z) : ratio (e.trans e') = ratio e * ratio e' := by
  -- If `X` is trivial, then so is `Y`, otherwise we apply `Dilation.ratio_comp'`
  by_cases hX : ∀ x y : X, edist x y = 0 ∨ edist x y = ∞
  · have hY : ∀ x y : Y, edistedist x y = 0 ∨ edist x y = ∞ := e.surjective.forall₂.2 fun x y ↦ by
      refine (hX x y).imp (fun h ↦ ?_) fun h ↦ ?_ <;> simp [*, Dilation.ratio_ne_zero]
    simp [Dilation.ratio_of_trivial, *]
  push_neg at hX
  exact (Dilation.ratio_comp' (g := e'.toDilation) (f := e.toDilation) hX).trans (mul_comm _ _)

Composition of Dilation Equivalences Preserves Ratio Product

Informal description

For any dilation equivalences $e \colon X \simeq^d Y$ and $e' \colon Y \simeq^d Z$ between pseudo-emetric spaces, the ratio of the composition $e' \circ e$ is equal to the product of the ratios of $e$ and $e'$, i.e., $\text{ratio}(e' \circ e) = \text{ratio}(e) \cdot \text{ratio}(e')$.

DilationEquiv.ratio_symm theorem

(e : X ≃ᵈ Y) : ratio e.symm = (ratio e)⁻¹

Full source

@[simp]
theorem ratio_symm (e : X ≃ᵈ Y) : ratio e.symm = (ratio e)⁻¹ :=
  eq_inv_of_mul_eq_one_left <| by rw [← ratio_trans, symm_trans_self, ratio_refl]

Inverse Dilation Equivalence Has Reciprocal Ratio: $\text{ratio}(e^{-1}) = (\text{ratio}(e))^{-1}$

Informal description

For any dilation equivalence $e \colon X \simeq^d Y$ between pseudo-emetric spaces $X$ and $Y$, the dilation ratio of the inverse equivalence $e^{-1}$ is the multiplicative inverse of the dilation ratio of $e$, i.e., $\text{ratio}(e^{-1}) = (\text{ratio}(e))^{-1}$.

DilationEquiv.instGroup instance

: Group (X ≃ᵈ X)

Full source

instance : Group (X ≃ᵈ X) where
  mul e e' := e'.trans e
  mul_assoc _ _ _ := rfl
  one := refl _
  one_mul _ := rfl
  mul_one _ := rfl
  inv := symm
  inv_mul_cancel := self_trans_symm

Group Structure of Dilation Equivalences

Informal description

The set of dilation equivalences on a pseudo-emetric space $X$ forms a group under composition, where the group operation is given by composition of equivalences, the identity element is the identity dilation equivalence, and the inverse of an equivalence is its inverse dilation equivalence.

DilationEquiv.mul_def theorem

(e e' : X ≃ᵈ X) : e * e' = e'.trans e

Full source

theorem mul_def (e e' : X ≃ᵈ X) : e * e' = e'.trans e := rfl

Group Multiplication of Dilation Equivalences as Composition

Informal description

For any two dilation equivalences $e$ and $e'$ on a pseudo-emetric space $X$, the group multiplication $e * e'$ is equal to the composition $e' \circ e$ (denoted as `e'.trans e` in the formal statement), where the composition is performed as dilation equivalences.

DilationEquiv.one_def theorem

: (1 : X ≃ᵈ X) = refl X

Full source

theorem one_def : (1 : X ≃ᵈ X) = refl X := rfl

Identity Dilation Equivalence is Group Identity

Informal description

The identity element of the group of dilation equivalences on a pseudo-emetric space $X$ is equal to the identity dilation equivalence, which is the reflexive dilation equivalence on $X$.

DilationEquiv.inv_def theorem

(e : X ≃ᵈ X) : e⁻¹ = e.symm

Full source

theorem inv_def (e : X ≃ᵈ X) : e⁻¹ = e.symm := rfl

Inverse of Dilation Equivalence is its Symmetric

Informal description

For any dilation equivalence $e \colon X \simeq^d X$ on a pseudo-emetric space $X$, the inverse $e^{-1}$ is equal to the symmetric dilation equivalence $e.\text{symm}$.

DilationEquiv.coe_mul theorem

(e e' : X ≃ᵈ X) : ⇑(e * e') = e ∘ e'

Full source

@[simp] theorem coe_mul (e e' : X ≃ᵈ X) : ⇑(e * e') = e ∘ e' := rfl

Composition of Dilation Equivalences as Function Composition

Informal description

For any two dilation equivalences $e$ and $e'$ on a pseudo-emetric space $X$, the underlying function of their composition $e * e'$ is equal to the composition of their underlying functions, i.e., $(e * e')(x) = e(e'(x))$ for all $x \in X$.

DilationEquiv.coe_one theorem

: ⇑(1 : X ≃ᵈ X) = id

Full source

@[simp] theorem coe_one : ⇑(1 : X ≃ᵈ X) = id := rfl

Identity Dilation Equivalence is the Identity Function

Informal description

The identity dilation equivalence on a pseudo-emetric space $X$ is equal to the identity function $\text{id} \colon X \to X$.

DilationEquiv.coe_inv theorem

(e : X ≃ᵈ X) : ⇑(e⁻¹) = e.symm

Full source

theorem coe_inv (e : X ≃ᵈ X) : ⇑(e⁻¹) = e.symm := rfl

Inverse Dilation Equivalence as Symmetric Equivalence

Informal description

For any dilation equivalence $e \colon X \simeq^d X$ on a pseudo-emetric space $X$, the underlying function of the inverse $e^{-1}$ is equal to the underlying function of the symmetric dilation equivalence $e^{\text{symm}}$.

DilationEquiv.ratioHom definition

: (X ≃ᵈ X) →* ℝ≥0

Full source

/-- `Dilation.ratio` as a monoid homomorphism. -/
noncomputable def ratioHom : (X ≃ᵈ X) →* ℝ≥0 where
  toFun := Dilation.ratio
  map_one' := ratio_refl
  map_mul' _ _ := (ratio_trans _ _).trans (mul_comm _ _)

Dilation ratio as a monoid homomorphism

Informal description

The function `DilationEquiv.ratioHom` is a monoid homomorphism from the group of dilation equivalences on a pseudo-emetric space $X$ to the multiplicative monoid of non-negative real numbers, mapping each dilation equivalence to its dilation ratio. Specifically, it satisfies: 1. The identity dilation equivalence maps to $1$ 2. The composition of two dilation equivalences maps to the product of their individual ratios (with the order of multiplication reversed)

DilationEquiv.ratio_inv theorem

(e : X ≃ᵈ X) : ratio (e⁻¹) = (ratio e)⁻¹

Full source

@[simp]
theorem ratio_inv (e : X ≃ᵈ X) : ratio (e⁻¹) = (ratio e)⁻¹ := ratio_symm e

Inverse Dilation Equivalence Has Reciprocal Ratio: $\text{ratio}(e^{-1}) = (\text{ratio}(e))^{-1}$

Informal description

For any dilation equivalence $e \colon X \simeq^d X$ on a pseudo-emetric space $X$, the dilation ratio of the inverse equivalence $e^{-1}$ is the multiplicative inverse of the dilation ratio of $e$, i.e., $\text{ratio}(e^{-1}) = (\text{ratio}(e))^{-1}$.

DilationEquiv.ratio_pow theorem

(e : X ≃ᵈ X) (n : ℕ) : ratio (e ^ n) = ratio e ^ n

Full source

@[simp]
theorem ratio_pow (e : X ≃ᵈ X) (n : ℕ) : ratio (e ^ n) = ratio e ^ n :=
  ratioHom.map_pow _ _

Dilation Ratio Preserved under Powers: $\text{ratio}(e^n) = \text{ratio}(e)^n$

Informal description

For any dilation equivalence $e \colon X \simeq^d X$ on a pseudo-emetric space $X$ and any natural number $n$, the dilation ratio of the $n$-th power of $e$ is equal to the $n$-th power of the dilation ratio of $e$, i.e., $\text{ratio}(e^n) = (\text{ratio}(e))^n$.

DilationEquiv.ratio_zpow theorem

(e : X ≃ᵈ X) (n : ℤ) : ratio (e ^ n) = ratio e ^ n

Full source

@[simp]
theorem ratio_zpow (e : X ≃ᵈ X) (n : ℤ) : ratio (e ^ n) = ratio e ^ n :=
  ratioHom.map_zpow _ _

Dilation Ratio Preserves Integer Powers: $\text{ratio}(e^n) = \text{ratio}(e)^n$

Informal description

For any dilation equivalence $e \colon X \simeq^d X$ on a pseudo-emetric space $X$ and any integer $n$, the dilation ratio of $e^n$ equals the $n$-th power of the dilation ratio of $e$, i.e., $\text{ratio}(e^n) = (\text{ratio}(e))^n$.

DilationEquiv.toPerm definition

: (X ≃ᵈ X) →* Equiv.Perm X

Full source

/-- `DilationEquiv.toEquiv` as a monoid homomorphism. -/
@[simps]
def toPerm : (X ≃ᵈ X) →* Equiv.Perm X where
  toFun e := e.1
  map_mul' _ _ := rfl
  map_one' := rfl

Dilation equivalence to permutation monoid homomorphism

Informal description

The function maps a dilation equivalence $e \colon X \simeq_{\text{dilation}} X$ to a permutation of $X$, preserving the group structure (i.e., it is a monoid homomorphism from the group of dilation equivalences to the group of permutations of $X$).

DilationEquiv.coe_pow theorem

(e : X ≃ᵈ X) (n : ℕ) : ⇑(e ^ n) = e^[n]

Full source

@[norm_cast]
theorem coe_pow (e : X ≃ᵈ X) (n : ℕ) : ⇑(e ^ n) = e^[n] := by
  rw [← coe_toEquiv, ← toPerm_apply, map_pow, Equiv.Perm.coe_pow]; rfl

Dilation Equivalence Power as Iteration: $(e^n)(x) = e^{[n]}(x)$

Informal description

For any dilation equivalence $e \colon X \simeq^d X$ on a pseudo-emetric space $X$ and any natural number $n$, the $n$-th power of $e$ as a dilation equivalence is equal to the $n$-th iterate of $e$ as a function, i.e., $(e^n)(x) = e^{[n]}(x)$ for all $x \in X$.

IsometryEquiv.toDilationEquiv definition

(e : X ≃ᵢ Y) : X ≃ᵈ Y

Full source

/-- Every isometry equivalence is a dilation equivalence of ratio `1`. -/
def _root_.IsometryEquiv.toDilationEquiv (e : X ≃ᵢ Y) : X ≃ᵈ Y where
  edist_eq' := ⟨1, one_ne_zero, by simpa using e.isometry⟩
  __ := e.toEquiv

Isometry equivalence as dilation equivalence with ratio 1

Informal description

Given an isometry equivalence $e : X \simeq_{\text{isometry}} Y$ between pseudo-emetric spaces $X$ and $Y$, the function maps $e$ to a dilation equivalence $X \simeq_{\text{dilation}} Y$ with scaling ratio $1$. This means that for all $x, y \in X$, the emetric distance between $e(x)$ and $e(y)$ equals the emetric distance between $x$ and $y$.

IsometryEquiv.toDilationEquiv_apply theorem

(e : X ≃ᵢ Y) (x : X) : e.toDilationEquiv x = e x

Full source

@[simp]
lemma _root_.IsometryEquiv.toDilationEquiv_apply (e : X ≃ᵢ Y) (x : X) :
    e.toDilationEquiv x = e x :=
  rfl

Application of Isometry Equivalence as Dilation Equivalence

Informal description

For any isometry equivalence $e : X \simeq_{\text{isometry}} Y$ between pseudo-emetric spaces $X$ and $Y$, and for any point $x \in X$, the dilation equivalence obtained from $e$ satisfies $(e.toDilationEquiv)(x) = e(x)$.

IsometryEquiv.toDilationEquiv_symm theorem

(e : X ≃ᵢ Y) : e.toDilationEquiv.symm = e.symm.toDilationEquiv

Full source

@[simp]
lemma _root_.IsometryEquiv.toDilationEquiv_symm (e : X ≃ᵢ Y) :
    e.toDilationEquiv.symm = e.symm.toDilationEquiv :=
  rfl

Inverse of Isometry-Induced Dilation Equivalence

Informal description

For any isometry equivalence $e \colon X \simeq_{\text{isometry}} Y$ between pseudo-emetric spaces $X$ and $Y$, the inverse of the dilation equivalence obtained from $e$ is equal to the dilation equivalence obtained from the inverse isometry equivalence $e^{-1}$.

IsometryEquiv.toDilationEquiv_toDilation theorem

(e : X ≃ᵢ Y) : (e.toDilationEquiv.toDilation : X →ᵈ Y) = e.isometry.toDilation

Full source

@[simp]
lemma _root_.IsometryEquiv.toDilationEquiv_toDilation (e : X ≃ᵢ Y) :
    (e.toDilationEquiv.toDilation : X →ᵈ Y) = e.isometry.toDilation :=
  rfl

Dilation structure preservation under isometry equivalence conversion

Informal description

For any isometry equivalence $e : X \simeq_{\text{isometry}} Y$ between pseudo-emetric spaces $X$ and $Y$, the underlying dilation of the induced dilation equivalence $e.toDilationEquiv$ is equal to the dilation induced by the isometry $e.isometry$.

IsometryEquiv.toDilationEquiv_ratio theorem

(e : X ≃ᵢ Y) : ratio e.toDilationEquiv = 1

Full source

@[simp]
lemma _root_.IsometryEquiv.toDilationEquiv_ratio (e : X ≃ᵢ Y) : ratio e.toDilationEquiv = 1 := by
  rw [← ratio_toDilation, IsometryEquiv.toDilationEquiv_toDilation, Isometry.toDilation_ratio]

Dilation Ratio of Isometry-Induced Dilation Equivalence is 1

Informal description

For any isometry equivalence $e \colon X \simeq_{\text{isometry}} Y$ between pseudo-emetric spaces $X$ and $Y$, the dilation ratio of the induced dilation equivalence $e.toDilationEquiv$ is equal to $1$.

DilationEquiv.toHomeomorph definition

(e : X ≃ᵈ Y) : X ≃ₜ Y

Full source

/-- Reinterpret a `DilationEquiv` as a homeomorphism. -/
def toHomeomorph (e : X ≃ᵈ Y) : X ≃ₜ Y where
  continuous_toFun := Dilation.toContinuous e
  continuous_invFun := Dilation.toContinuous e.symm
  __ := e.toEquiv

Homeomorphism induced by a dilation equivalence

Informal description

Given a dilation equivalence $e$ between pseudo-emetric spaces $X$ and $Y$, the function $e$ can be reinterpreted as a homeomorphism between $X$ and $Y$. This means that $e$ is a continuous bijection with a continuous inverse, preserving the topological structure of the spaces.

DilationEquiv.coe_toHomeomorph theorem

(e : X ≃ᵈ Y) : ⇑e.toHomeomorph = e

Full source

@[simp]
lemma coe_toHomeomorph (e : X ≃ᵈ Y) : ⇑e.toHomeomorph = e :=
  rfl

Homeomorphism Function Coincides with Dilation Equivalence

Informal description

For any dilation equivalence $e$ between pseudo-emetric spaces $X$ and $Y$, the underlying function of the induced homeomorphism $e.toHomeomorph$ is equal to $e$ itself.

DilationEquiv.toHomeomorph_symm theorem

(e : X ≃ᵈ Y) : e.toHomeomorph.symm = e.symm.toHomeomorph

Full source

@[simp]
lemma toHomeomorph_symm (e : X ≃ᵈ Y) : e.toHomeomorph.symm = e.symm.toHomeomorph :=
  rfl

Inverse Homeomorphism of Dilation Equivalence

Informal description

For any dilation equivalence $e \colon X \simeq^d Y$ between pseudo-emetric spaces $X$ and $Y$, the inverse of the induced homeomorphism $e.toHomeomorph$ is equal to the homeomorphism induced by the inverse dilation equivalence $e.symm$.

DilationEquiv.map_cobounded theorem

(e : F) : map e (cobounded X) = cobounded Y

Full source

@[simp]
lemma map_cobounded (e : F) : map e (cobounded X) = cobounded Y := by
  rw [← Dilation.comap_cobounded e, map_comap_of_surjective (EquivLike.surjective e)]

Dilation Equivalence Preserves Cobounded Filters

Informal description

For any dilation equivalence $e \colon X \to Y$ between pseudo-emetric spaces $X$ and $Y$, the image of the cobounded filter on $X$ under $e$ is equal to the cobounded filter on $Y$. In other words, $e$ maps sets with finite complements in $X$ to sets with finite complements in $Y$.

TODO