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 pseudo_metric_space
and we specialize to metric_space
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 distances.
An isometry preserves edistances.
An isometry preserves distances.
An isometry from an emetric space is injective
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 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 a metric space is a uniform embedding
An isometry from a metric space is an embedding
An isometry from a complete emetric space is a closed embedding
An isometry preserves the diameter in pseudometric spaces.
α
and β
are isometric if there is an isometric bijection between them.
Alternative constructor for isometric bijections, taking as input an isometry, and a right inverse.
Equations
- isometric.mk' f g hfg hf = {to_equiv := {to_fun := f, inv_fun := g, left_inv := _, right_inv := hfg}, isometry_to_fun := hf}
The identity isometry of a space.
Equations
- isometric.refl α = {to_equiv := {to_fun := (equiv.refl α).to_fun, inv_fun := (equiv.refl α).inv_fun, left_inv := _, right_inv := _}, isometry_to_fun := _}
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
- isometric.simps.symm_apply h = ⇑(h.symm)
The (bundled) homeomorphism associated to an isometric isomorphism.
Equations
- h.to_homeomorph = {to_equiv := h.to_equiv, continuous_to_fun := _, continuous_inv_fun := _}
The group of isometries.
Equations
- isometric.group = {mul := λ (e₁ e₂ : α ≃ᵢ α), e₂.trans e₁, mul_assoc := _, one := isometric.refl α _inst_1, one_mul := _, mul_one := _, npow := div_inv_monoid.npow._default (isometric.refl α) (λ (e₁ e₂ : α ≃ᵢ α), e₂.trans e₁) isometric.group._proof_4 isometric.group._proof_5, npow_zero' := _, npow_succ' := _, inv := isometric.symm _inst_1, div := div_inv_monoid.div._default (λ (e₁ e₂ : α ≃ᵢ α), e₂.trans e₁) isometric.group._proof_8 (isometric.refl α) isometric.group._proof_9 isometric.group._proof_10 (div_inv_monoid.npow._default (isometric.refl α) (λ (e₁ e₂ : α ≃ᵢ α), e₂.trans e₁) isometric.group._proof_4 isometric.group._proof_5) isometric.group._proof_11 isometric.group._proof_12 isometric.symm, div_eq_mul_inv := _, zpow := div_inv_monoid.zpow._default (λ (e₁ e₂ : α ≃ᵢ α), e₂.trans e₁) isometric.group._proof_14 (isometric.refl α) isometric.group._proof_15 isometric.group._proof_16 (div_inv_monoid.npow._default (isometric.refl α) (λ (e₁ e₂ : α ≃ᵢ α), e₂.trans e₁) isometric.group._proof_4 isometric.group._proof_5) isometric.group._proof_17 isometric.group._proof_18 isometric.symm, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _}
An isometry induces an isometric isomorphism between the source space and the range of the isometry.
Equations
- h.isometric_on_range = {to_equiv := equiv.of_injective f _, isometry_to_fun := _}