Dilation equivalence

In this file we define DilationEquiv X Y, a type of bundled equivalences between X and Ysuch thatedist (f x) (f y) = r * edist x yfor somer : ℝ≥0, r ≠ 0`.

We also develop basic API about these equivalences.

TODO

• Add missing lemmas (compare to other *Equiv structures).
• [after-port] Add DilationEquivInstance for IsometryEquiv.

class DilationEquivClass (F : Type u_1) (X : outParam (Type u_2)) (Y : outParam (Type u_3)) [PseudoEMetricSpace X] [PseudoEMetricSpace Y] [EquivLike F X Y] : Prop

Typeclass saying that F is a type of bundled equivalences such that all e : F are dilations.

• edist_eq' (f : F) : ∃ (r : NNReal), r ≠ 0 ∧ ∀ (x y : X), edist (f x) (f y) = ↑r * edist x y

@[instance 100]

instance instDilationClassOfDilationEquivClass (F : Type u_1) (X : outParam (Type u_2)) (Y : outParam (Type u_3)) [PseudoEMetricSpace X] [PseudoEMetricSpace Y] [EquivLike F X Y] [DilationEquivClass F X Y] : DilationClass F X Y

structure DilationEquiv (X : Type u_1) (Y : Type u_2) [PseudoEMetricSpace X] [PseudoEMetricSpace Y] extends X ≃ Y, X →ᵈ Y : Type (max u_1 u_2)

Type of equivalences X ≃ Y such that ∀ x y, edist (f x) (f y) = r * edist x y for some r : ℝ≥0, r ≠ 0.

• toFun : X → Y
• invFun : Y → X
• left_inv : Function.LeftInverse self.invFun self.toFun
• right_inv : Function.RightInverse self.invFun self.toFun
• edist_eq' : ∃ (r : NNReal), r ≠ 0 ∧ ∀ (x y : X), edist (self.toFun x) (self.toFun y) = ↑r * edist x y

def «term_≃ᵈ_» : Lean.TrailingParserDescr

Type of equivalences X ≃ Y such that ∀ x y, edist (f x) (f y) = r * edist x y for some r : ℝ≥0, r ≠ 0.

Equations

• «term_≃ᵈ_» = Lean.ParserDescr.trailingNode `«term_≃ᵈ_» 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≃ᵈ ") (Lean.ParserDescr.cat `term 26))

instance DilationEquiv.instEquivLike {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] : EquivLike (X ≃ᵈ Y) X Y

Equations

• DilationEquiv.instEquivLike = { coe := fun (f : X ≃ᵈ Y) => ⇑f.toEquiv, inv := fun (f : X ≃ᵈ Y) => ⇑f.symm, left_inv := ⋯, right_inv := ⋯, coe_injective' := ⋯ }

instance DilationEquiv.instDilationEquivClass {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] : DilationEquivClass (X ≃ᵈ Y) X Y

@[simp]

theorem DilationEquiv.coe_toEquiv {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵈ Y) : ⇑e.toEquiv = ⇑e

theorem DilationEquiv.ext {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] {e e' : X ≃ᵈ Y} (h : ∀ (x : X), e x = e' x) : e = e'

def DilationEquiv.symm {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵈ Y) : Y ≃ᵈ X

Inverse DilationEquiv.

Equations

• e.symm = { toEquiv := e.symm, edist_eq' := ⋯ }

@[simp]

theorem DilationEquiv.symm_symm {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵈ Y) : e.symm.symm = e

theorem DilationEquiv.symm_bijective {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] : Function.Bijective DilationEquiv.symm

@[simp]

theorem DilationEquiv.apply_symm_apply {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵈ Y) (x : Y) : e (e.symm x) = x

@[simp]

theorem DilationEquiv.symm_apply_apply {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵈ Y) (x : X) : e.symm (e x) = x

def DilationEquiv.Simps.symm_apply {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵈ Y) : Y → X

See Note [custom simps projection].

Equations

• DilationEquiv.Simps.symm_apply e = ⇑e.symm

theorem DilationEquiv.ratio_toDilation {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵈ Y) : Dilation.ratio e.toDilation = Dilation.ratio e

def DilationEquiv.refl (X : Type u_4) [PseudoEMetricSpace X] : X ≃ᵈ X

Identity map as a DilationEquiv.

Equations

• DilationEquiv.refl X = { toEquiv := Equiv.refl X, edist_eq' := ⋯ }

@[simp]

theorem DilationEquiv.refl_apply (X : Type u_4) [PseudoEMetricSpace X] : ⇑(DilationEquiv.refl X) = id

@[simp]

theorem DilationEquiv.refl_symm {X : Type u_1} [PseudoEMetricSpace X] : (DilationEquiv.refl X).symm = DilationEquiv.refl X

@[simp]

theorem DilationEquiv.ratio_refl {X : Type u_1} [PseudoEMetricSpace X] : Dilation.ratio (DilationEquiv.refl X) = 1

def DilationEquiv.trans {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] [PseudoEMetricSpace Z] (e₁ : X ≃ᵈ Y) (e₂ : Y ≃ᵈ Z) : X ≃ᵈ Z

Composition of DilationEquivs.

Equations

• e₁.trans e₂ = { toEquiv := e₁.trans e₂.toEquiv, edist_eq' := ⋯ }

@[simp]

theorem DilationEquiv.trans_apply {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] [PseudoEMetricSpace Z] (e₁ : X ≃ᵈ Y) (e₂ : Y ≃ᵈ Z) : ⇑(e₁.trans e₂) = ⇑e₂ ∘ ⇑e₁

@[simp]

theorem DilationEquiv.refl_trans {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵈ Y) : (DilationEquiv.refl X).trans e = e

@[simp]

theorem DilationEquiv.trans_refl {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵈ Y) : e.trans (DilationEquiv.refl Y) = e

@[simp]

theorem DilationEquiv.symm_trans_self {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵈ Y) : e.symm.trans e = DilationEquiv.refl Y

@[simp]

theorem DilationEquiv.self_trans_symm {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵈ Y) : e.trans e.symm = DilationEquiv.refl X

theorem DilationEquiv.surjective {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵈ Y) : Function.Surjective ⇑e

theorem DilationEquiv.bijective {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵈ Y) : Function.Bijective ⇑e

theorem DilationEquiv.injective {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵈ Y) : Function.Injective ⇑e

@[simp]

theorem DilationEquiv.ratio_trans {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] [PseudoEMetricSpace Z] (e : X ≃ᵈ Y) (e' : Y ≃ᵈ Z) : Dilation.ratio (e.trans e') = Dilation.ratio e * Dilation.ratio e'

@[simp]

theorem DilationEquiv.ratio_symm {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵈ Y) : Dilation.ratio e.symm = (Dilation.ratio e)⁻¹

instance DilationEquiv.instGroup {X : Type u_1} [PseudoEMetricSpace X] : Group (X ≃ᵈ X)

Equations

• DilationEquiv.instGroup = Group.mk ⋯

theorem DilationEquiv.mul_def {X : Type u_1} [PseudoEMetricSpace X] (e e' : X ≃ᵈ X) : e * e' = e'.trans e

theorem DilationEquiv.one_def {X : Type u_1} [PseudoEMetricSpace X] : 1 = DilationEquiv.refl X

theorem DilationEquiv.inv_def {X : Type u_1} [PseudoEMetricSpace X] (e : X ≃ᵈ X) : e⁻¹ = e.symm

@[simp]

theorem DilationEquiv.coe_mul {X : Type u_1} [PseudoEMetricSpace X] (e e' : X ≃ᵈ X) : ⇑(e * e') = ⇑e ∘ ⇑e'

@[simp]

theorem DilationEquiv.coe_one {X : Type u_1} [PseudoEMetricSpace X] : ⇑1 = id

theorem DilationEquiv.coe_inv {X : Type u_1} [PseudoEMetricSpace X] (e : X ≃ᵈ X) : ⇑e⁻¹ = ⇑e.symm

noncomputable def DilationEquiv.ratioHom {X : Type u_1} [PseudoEMetricSpace X] : (X ≃ᵈ X) →* NNReal

Dilation.ratio as a monoid homomorphism.

Equations

• DilationEquiv.ratioHom = { toFun := Dilation.ratio, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem DilationEquiv.ratio_inv {X : Type u_1} [PseudoEMetricSpace X] (e : X ≃ᵈ X) : Dilation.ratio e⁻¹ = (Dilation.ratio e)⁻¹

@[simp]

theorem DilationEquiv.ratio_pow {X : Type u_1} [PseudoEMetricSpace X] (e : X ≃ᵈ X) (n : ℕ) : Dilation.ratio (e ^ n) = Dilation.ratio e ^ n

@[simp]

theorem DilationEquiv.ratio_zpow {X : Type u_1} [PseudoEMetricSpace X] (e : X ≃ᵈ X) (n : ℤ) : Dilation.ratio (e ^ n) = Dilation.ratio e ^ n

def DilationEquiv.toPerm {X : Type u_1} [PseudoEMetricSpace X] : (X ≃ᵈ X) →* Equiv.Perm X

DilationEquiv.toEquiv as a monoid homomorphism.

Equations

• DilationEquiv.toPerm = { toFun := fun (e : X ≃ᵈ X) => e.toEquiv, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem DilationEquiv.toPerm_apply {X : Type u_1} [PseudoEMetricSpace X] (e : X ≃ᵈ X) : DilationEquiv.toPerm e = e.toEquiv

theorem DilationEquiv.coe_pow {X : Type u_1} [PseudoEMetricSpace X] (e : X ≃ᵈ X) (n : ℕ) : ⇑(e ^ n) = (⇑e)^[n]

def IsometryEquiv.toDilationEquiv {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵢ Y) : X ≃ᵈ Y

Every isometry equivalence is a dilation equivalence of ratio 1.

Equations

• e.toDilationEquiv = { toEquiv := e.toEquiv, edist_eq' := ⋯ }

@[simp]

theorem IsometryEquiv.toDilationEquiv_apply {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵢ Y) (x : X) : e.toDilationEquiv x = e x

@[simp]

theorem IsometryEquiv.toDilationEquiv_symm {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵢ Y) : e.toDilationEquiv.symm = e.symm.toDilationEquiv

@[simp]

theorem IsometryEquiv.toDilationEquiv_toDilation {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵢ Y) : e.toDilationEquiv.toDilation = Isometry.toDilation ⇑e ⋯

@[simp]

theorem IsometryEquiv.toDilationEquiv_ratio {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵢ Y) : Dilation.ratio e.toDilationEquiv = 1

def DilationEquiv.toHomeomorph {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵈ Y) : X ≃ₜ Y

Reinterpret a DilationEquiv as a homeomorphism.

Equations

• e.toHomeomorph = { toEquiv := e.toEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem DilationEquiv.coe_toHomeomorph {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵈ Y) : ⇑e.toHomeomorph = ⇑e

@[simp]

theorem DilationEquiv.toHomeomorph_symm {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵈ Y) : e.toHomeomorph.symm = e.symm.toHomeomorph

@[simp]

theorem DilationEquiv.map_cobounded {X : Type u_1} {Y : Type u_2} {F : Type u_3} [PseudoMetricSpace X] [PseudoMetricSpace Y] [EquivLike F X Y] [DilationEquivClass F X Y] (e : F) : Filter.map (⇑e) (Bornology.cobounded X) = Bornology.cobounded Y