Dilation equivalence #
In this file we define DilationEquiv X Y
, a type of bundled equivalences between X
and Ysuch that
edist (f x) (f y) = r * edist x yfor some
r : ℝ≥0,
r ≠ 0`.
We also develop basic API about these equivalences.
TODO #
- Add missing lemmas (compare to other
*Equiv
structures). - [after-port] Add
DilationEquivInstance
forIsometryEquiv
.
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)
- 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
Typeclass saying that F
is a type of bundled equivalences such that all e : F
are
dilations.
Instances
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
structure
DilationEquiv
(X : Type u_1)
(Y : Type u_2)
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
extends
Equiv
:
Type (max u_1 u_2)
- 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, r ≠ 0 ∧ ∀ (x y : X), edist (Equiv.toFun s.toEquiv x) (Equiv.toFun s.toEquiv y) = ↑r * edist x y
Type of equivalences X ≃ Y
such that ∀ x y, edist (f x) (f y) = r * edist x y
for some
r : ℝ≥0
, r ≠ 0
.
Instances For
instance
DilationEquiv.instDilationEquivClassDilationEquiv
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
:
DilationEquivClass (X ≃ᵈ Y) X Y
instance
DilationEquiv.instCoeFunDilationEquivForAll
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace 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 : 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
.
Instances For
@[simp]
theorem
DilationEquiv.symm_symm
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
(e : X ≃ᵈ Y)
:
@[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].
Instances For
@[simp]
theorem
DilationEquiv.refl_apply
(X : Type u_4)
[PseudoEMetricSpace X]
:
↑(DilationEquiv.refl X) = id
Identity map as a DilationEquiv
.
Instances For
@[simp]
@[simp]
@[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 DilationEquiv
s.
Instances For
@[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)
:
@[simp]
theorem
DilationEquiv.self_trans_symm
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
(e : X ≃ᵈ Y)
:
theorem
DilationEquiv.surjective
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
(e : X ≃ᵈ Y)
:
theorem
DilationEquiv.bijective
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
(e : X ≃ᵈ Y)
:
theorem
DilationEquiv.injective
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
(e : X ≃ᵈ Y)
:
@[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)
:
theorem
DilationEquiv.mul_def
{X : Type u_1}
[PseudoEMetricSpace X]
(e : X ≃ᵈ X)
(e' : X ≃ᵈ X)
:
e * e' = DilationEquiv.trans e' e
@[simp]
theorem
DilationEquiv.coe_inv
{X : Type u_1}
[PseudoEMetricSpace X]
(e : X ≃ᵈ X)
:
↑e⁻¹ = ↑(DilationEquiv.symm e)
Dilation.ratio
as a monoid homomorphism.
Instances For
@[simp]
@[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
DilationEquiv.toEquiv
as a monoid homomorphism.