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.

source

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

Instances

source

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

source

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

source

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))

source

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' := ⋯ }

source

instance DilationEquiv.instDilationEquivClass {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] :

DilationEquivClass (X ≃ᵈ Y) X Y

source

@[simp]

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

⇑e.toEquiv = ⇑e

source

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'

source

theorem DilationEquiv.ext_iff {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] {e e' : X ≃ᵈ Y} :

e = e' ↔ ∀ (x : X), e x = e' x

source

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' := ⋯ }

source

@[simp]

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

e.symm.symm = e

source

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

Function.Bijective symm

source

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

source

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

source

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

source

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

source

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' := ⋯ }

source

@[simp]

theorem DilationEquiv.refl_apply (X : Type u_4) [PseudoEMetricSpace X] :

⇑(refl X) = id

source

@[simp]

theorem DilationEquiv.refl_symm {X : Type u_1} [PseudoEMetricSpace X] :

(refl X).symm = refl X

source

@[simp]

theorem DilationEquiv.ratio_refl {X : Type u_1} [PseudoEMetricSpace X] :

Dilation.ratio (refl X) = 1

source

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' := ⋯ }

source

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

source

@[simp]

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

(refl X).trans e = e

source

@[simp]

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

e.trans (refl Y) = e

source

@[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 = refl Y

source

@[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 = refl X

source

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

Function.Surjective ⇑e

source

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

Function.Bijective ⇑e

source

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

Function.Injective ⇑e

source

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

source

@[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)⁻¹

source

instance DilationEquiv.instGroup {X : Type u_1} [PseudoEMetricSpace X] :

Group (X ≃ᵈ X)

Equations

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

source

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

e * e' = e'.trans e

source

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

1 = refl X

source

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

e⁻¹ = e.symm

source

@[simp]

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

⇑(e * e') = ⇑e ∘ ⇑e'

source

@[simp]

theorem DilationEquiv.coe_one {X : Type u_1} [PseudoEMetricSpace X] :

⇑1 = id

source

theorem DilationEquiv.coe_inv {X : Type u_1} [PseudoEMetricSpace X] (e : X ≃ᵈ X) :

⇑e⁻¹ = ⇑e.symm

source

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' := ⋯ }

source

@[simp]

theorem DilationEquiv.ratio_inv {X : Type u_1} [PseudoEMetricSpace X] (e : X ≃ᵈ X) :

Dilation.ratio e⁻¹ = (Dilation.ratio e)⁻¹

source

@[simp]

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

Dilation.ratio (e ^ n) = Dilation.ratio e ^ n

source

@[simp]

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

Dilation.ratio (e ^ n) = Dilation.ratio e ^ n

source

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' := ⋯ }

source

@[simp]

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

toPerm e = e.toEquiv

source

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

⇑(e ^ n) = (⇑e)^[n]

source

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' := ⋯ }

source

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

source

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

source

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

source

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

source

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 := ⋯ }

source

@[simp]

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

⇑e.toHomeomorph = ⇑e

source

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

source

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

Documentation

Mathlib.Topology.MetricSpace.DilationEquiv

Dilation equivalence #

TODO #