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 instDilationClassToFunLike (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

Equations

• (_ : DilationClass F X Y) = (_ : DilationClass F X Y)

structure DilationEquiv (X : Type u_1) (Y : Type u_2) [PseudoEMetricSpace X] [PseudoEMetricSpace Y] extends Equiv : 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.toEquiv.toFun x) (self.toEquiv.toFun y) = ↑r * edist x y

def «term_≃ᵈ_» : Lean.TrailingParserDescr

Equations

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• (_ : DilationEquivClass (X ≃ᵈ Y) X Y) = (_ : DilationEquivClass (X ≃ᵈ Y) X Y)

instance DilationEquiv.instCoeFunDilationEquivForAll {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] : CoeFun (X ≃ᵈ Y) fun (x : X ≃ᵈ Y) => X → Y

Equations

• DilationEquiv.instCoeFunDilationEquivForAll = { coe := fun (f : X ≃ᵈ Y) => ⇑f }

@[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 : X ≃ᵈ Y} {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

• DilationEquiv.symm e = { toEquiv := e.symm, edist_eq' := (_ : ∃ (r : NNReal), r ≠ 0 ∧ ∀ (x y : Y), edist (e.symm.toFun x) (e.symm.toFun y) = ↑r * edist x y) }

@[simp]

theorem DilationEquiv.symm_symm {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵈ Y) : DilationEquiv.symm (DilationEquiv.symm e) = 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 ((DilationEquiv.symm e) 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) : (DilationEquiv.symm e) (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 = ⇑(DilationEquiv.symm e)

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

@[simp]

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

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

Identity map as a DilationEquiv.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

@[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) : ⇑(DilationEquiv.trans e₁ e₂) = ⇑e₂ ∘ ⇑e₁

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

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

theorem DilationEquiv.trans_refl {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵈ Y) : DilationEquiv.trans e (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) : DilationEquiv.trans (DilationEquiv.symm e) 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) : DilationEquiv.trans e (DilationEquiv.symm e) = 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 (DilationEquiv.trans e 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 (DilationEquiv.symm e) = (Dilation.ratio e)⁻¹

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

Equations

• DilationEquiv.instGroupDilationEquiv = Group.mk (_ : ∀ (e : X ≃ᵈ X), DilationEquiv.trans e (DilationEquiv.symm e) = DilationEquiv.refl X)

theorem DilationEquiv.mul_def {X : Type u_1} [PseudoEMetricSpace X] (e : X ≃ᵈ X) (e' : X ≃ᵈ X) : e * e' = DilationEquiv.trans e' 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⁻¹ = DilationEquiv.symm e

@[simp]

theorem DilationEquiv.coe_mul {X : Type u_1} [PseudoEMetricSpace X] (e : X ≃ᵈ X) (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⁻¹ = ⇑(DilationEquiv.symm e)

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

Dilation.ratio as a monoid homomorphism.

Equations

• One or more equations did not get rendered due to their size.

@[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

@[simp]

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

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

DilationEquiv.toEquiv as a monoid homomorphism.

Equations

• One or more equations did not get rendered due to their size.

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

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem IsometryEquiv.toDilationEquiv_ratio {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵢ Y) : Dilation.ratio (IsometryEquiv.toDilationEquiv e) = 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

• DilationEquiv.toHomeomorph e = let src := e.toEquiv; Homeomorph.mk src

@[simp]

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

@[simp]

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

@[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