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]
[EquivLike F X Y]
:
Typeclass saying that F
is a type of bundled equivalences such that all e : F
are
dilations.
Instances
@[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
Instances For
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
Instances For
instance
DilationEquiv.instEquivLike
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
:
Equations
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)
:
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)
:
theorem
DilationEquiv.ext_iff
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
{e e' : X ≃ᵈ Y}
:
def
DilationEquiv.symm
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
(e : X ≃ᵈ Y)
:
Inverse DilationEquiv
.
Equations
Instances For
@[simp]
theorem
DilationEquiv.symm_symm
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
(e : X ≃ᵈ Y)
:
theorem
DilationEquiv.symm_bijective
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
:
@[simp]
theorem
DilationEquiv.apply_symm_apply
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
(e : X ≃ᵈ Y)
(x : Y)
:
@[simp]
theorem
DilationEquiv.symm_apply_apply
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
(e : X ≃ᵈ Y)
(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
Instances For
theorem
DilationEquiv.ratio_toDilation
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
(e : X ≃ᵈ Y)
:
@[simp]
@[simp]
@[simp]
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)
:
Composition of DilationEquiv
s.
Equations
Instances For
@[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)
:
@[simp]
theorem
DilationEquiv.refl_trans
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
(e : X ≃ᵈ Y)
:
@[simp]
theorem
DilationEquiv.trans_refl
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
(e : X ≃ᵈ Y)
:
@[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)
:
@[simp]
theorem
DilationEquiv.ratio_symm
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
(e : X ≃ᵈ Y)
:
Equations
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
def
IsometryEquiv.toDilationEquiv
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
(e : X ≃ᵢ Y)
:
Every isometry equivalence is a dilation equivalence of ratio 1
.
Equations
Instances For
@[simp]
theorem
IsometryEquiv.toDilationEquiv_apply
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
(e : X ≃ᵢ Y)
(x : X)
:
@[simp]
theorem
IsometryEquiv.toDilationEquiv_symm
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
(e : X ≃ᵢ Y)
:
@[simp]
theorem
IsometryEquiv.toDilationEquiv_toDilation
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
(e : X ≃ᵢ Y)
:
@[simp]
theorem
IsometryEquiv.toDilationEquiv_ratio
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
(e : X ≃ᵢ Y)
:
def
DilationEquiv.toHomeomorph
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
(e : X ≃ᵈ Y)
:
Reinterpret a DilationEquiv
as a homeomorphism.
Equations
Instances For
@[simp]
theorem
DilationEquiv.coe_toHomeomorph
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
(e : X ≃ᵈ Y)
:
@[simp]
theorem
DilationEquiv.toHomeomorph_symm
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
(e : X ≃ᵈ Y)
:
@[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)
: