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] extends EquivLike : Type (max (max u_1 u_2) u_3)

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

• coe : F → X → Y
• inv : F → Y → X
• left_inv : ∀ (e : F), Function.LeftInverse (EquivLike.inv e) (EquivLike.coe e)
• right_inv : ∀ (e : F), Function.RightInverse (EquivLike.inv e) (EquivLike.coe e)
• coe_injective' : ∀ (e g : F), EquivLike.coe e = EquivLike.coe g → EquivLike.inv e = EquivLike.inv g → e = g
• edist_eq' : ∀ (f : F), ∃ (r : NNReal), r ≠ 0 ∧ ∀ (x y : X), edist (f x) (f y) = ↑r * edist x y

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

Equations

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

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 s.invFun s.toFun
• right_inv : Function.RightInverse s.invFun s.toFun
• edist_eq' : ∃ (r : NNReal), r ≠ 0 ∧ ∀ (x y : X), edist (Equiv.toFun s.toEquiv x) (Equiv.toFun s.toEquiv 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.instDilationEquivClassDilationEquiv {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] : DilationEquivClass (X ≃ᵈ Y) X Y

Equations

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

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 (Equiv.toFun e.symm x) (Equiv.toFun e.symm 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)

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

@[simp]

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