Isometries #
We define isometries, i.e., maps between emetric spaces that preserve the edistance (on metric spaces, these are exactly the maps that preserve distances), and prove their basic properties. We also introduce isometric bijections.
Since a lot of elementary properties don't require eq_of_dist_eq_zero
we start setting up the
theory for PseudoMetricSpace
and we specialize to MetricSpace
when needed.
An isometry (also known as isometric embedding) is a map preserving the edistance between pseudoemetric spaces, or equivalently the distance between pseudometric space.
Instances For
On pseudometric spaces, a map is an isometry if and only if it preserves nonnegative distances.
On pseudometric spaces, a map is an isometry if and only if it preserves distances.
An isometry preserves distances.
A map that preserves distances is an isometry
An isometry preserves non-negative distances.
A map that preserves non-negative distances is an isometry.
An isometry preserves edistances.
Any map on a subsingleton is an isometry
The identity is an isometry
The composition of isometries is an isometry.
An isometry from a metric space is a uniform continuous map
An isometry from a metric space is a uniform inducing map
An isometry is continuous.
The right inverse of an isometry is an isometry.
Isometries preserve the diameter in pseudoemetric spaces.
The injection from a subtype is an isometry
An isometry from an emetric space is injective
An isometry from an emetric space is a uniform embedding
Alias of Isometry.isUniformEmbedding
.
An isometry from an emetric space is a uniform embedding
An isometry from an emetric space is an embedding
An isometry from a complete emetric space is a closed embedding
An isometry preserves the diameter in pseudometric spaces.
A uniform embedding from a uniform space to a metric space is an isometry with respect to the induced metric space structure on the source space.
Alias of IsUniformEmbedding.to_isometry
.
A uniform embedding from a uniform space to a metric space is an isometry with respect to the induced metric space structure on the source space.
An embedding from a topological space to a metric space is an isometry with respect to the induced metric space structure on the source space.
α
and β
are isometric if there is an isometric bijection between them.
- toFun : α → β
- invFun : β → α
- left_inv : Function.LeftInverse self.invFun self.toFun
- right_inv : Function.RightInverse self.invFun self.toFun
- isometry_toFun : Isometry self.toFun
Instances For
α
and β
are isometric if there is an isometric bijection between them.
Equations
- «term_≃ᵢ_» = Lean.ParserDescr.trailingNode `term_≃ᵢ_ 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≃ᵢ ") (Lean.ParserDescr.cat `term 26))
Instances For
Alternative constructor for isometric bijections, taking as input an isometry, and a right inverse.
Equations
- IsometryEquiv.mk' f g hfg hf = { toFun := f, invFun := g, left_inv := ⋯, right_inv := hfg, isometry_toFun := hf }
Instances For
The identity isometry of a space.
Equations
- IsometryEquiv.refl α = { toEquiv := Equiv.refl α, isometry_toFun := ⋯ }
Instances For
The composition of two isometric isomorphisms, as an isometric isomorphism.
Equations
- h₁.trans h₂ = { toEquiv := h₁.trans h₂.toEquiv, isometry_toFun := ⋯ }
Instances For
The inverse of an isometric isomorphism, as an isometric isomorphism.
Equations
- h.symm = { toEquiv := h.symm, isometry_toFun := ⋯ }
Instances For
See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.
Equations
Instances For
See Note [custom simps projection]
Equations
- IsometryEquiv.Simps.symm_apply h = ⇑h.symm
Instances For
The (bundled) homeomorphism associated to an isometric isomorphism.
Equations
- h.toHomeomorph = { toEquiv := h.toEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Instances For
The group of isometries.
Equiv.funUnique
as an IsometryEquiv
.
Equations
- IsometryEquiv.funUnique ι α = { toEquiv := Equiv.funUnique ι α, isometry_toFun := ⋯ }
Instances For
piFinTwoEquiv
as an IsometryEquiv
.
Equations
- IsometryEquiv.piFinTwo α = { toEquiv := piFinTwoEquiv α, isometry_toFun := ⋯ }
Instances For
An isometry induces an isometric isomorphism between the source space and the range of the isometry.
Equations
- h.isometryEquivOnRange = { toEquiv := Equiv.ofInjective f ⋯, isometry_toFun := h }
Instances For
Post-composition by an isometry does not change the Lipschitz-property of a function.