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.
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
Alias of Isometry.piMap
.
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
Alias of Isometry.isUniformInducing
.
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
Alias of Isometry.isEmbedding
.
An isometry from an emetric space is an embedding
An isometry from a complete emetric space is a closed embedding
Alias of Isometry.isClosedEmbedding
.
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.
Alias of Topology.IsEmbedding.to_isometry
.
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
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))
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 }
The identity isometry of a space.
Equations
- IsometryEquiv.refl α = { toEquiv := Equiv.refl α, isometry_toFun := ⋯ }
The composition of two isometric isomorphisms, as an isometric isomorphism.
The inverse of an isometric isomorphism, as an isometric isomorphism.
See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.
Equations
See Note [custom simps projection]
Equations
The (bundled) homeomorphism associated to an isometric isomorphism.
Equations
- h.toHomeomorph = { toEquiv := h.toEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }
The group of isometries.
Equations
The natural isometry ∀ i, Y i ≃ᵢ ∀ j, Y (e.symm j)
obtained from a bijection ι ≃ ι'
of
fintypes. Equiv.piCongrLeft'
as an IsometryEquiv
.
Equations
- IsometryEquiv.piCongrLeft' e = { toEquiv := Equiv.piCongrLeft' Y e, isometry_toFun := ⋯ }
The natural isometry ∀ i, Y (e i) ≃ᵢ ∀ j, Y j
obtained from a bijection ι ≃ ι'
of fintypes.
Equiv.piCongrLeft
as an IsometryEquiv
.
Equations
The natural isometry (α ⊕ β → γ) ≃ᵢ (α → γ) × (β → γ)
between the type of maps on a sum of
fintypes α ⊕ β
and the pairs of functions on the types α
and β
.
Equiv.sumArrowEquivProdArrow
as an IsometryEquiv
.
Equations
- IsometryEquiv.sumArrowIsometryEquivProdArrow = { toEquiv := Equiv.sumArrowEquivProdArrow α β γ, isometry_toFun := ⋯ }
The natural IsometryEquiv
between (Fin m → α) × (Fin n → α)
and Fin (m + n) → α
.
Fin.appendEquiv
as an IsometryEquiv
.
Equations
- Fin.appendIsometry m n = { toEquiv := Fin.appendEquiv m n, isometry_toFun := ⋯ }
Equiv.funUnique
as an IsometryEquiv
.
Equations
- IsometryEquiv.funUnique ι α = { toEquiv := Equiv.funUnique ι α, isometry_toFun := ⋯ }
piFinTwoEquiv
as an IsometryEquiv
.
Equations
- IsometryEquiv.piFinTwo α = { toEquiv := piFinTwoEquiv α, isometry_toFun := ⋯ }
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 }
Post-composition by an isometry does not change the Lipschitz-property of a function.