Theorems · Definition · general topology
Isometry.isometryEquivOnRange
{α : Type u} →
{β : Type v} →
[inst : EMetricSpace α] → [inst_1 : PseudoEMetricSpace β] → {f : α → β} → Isometry f → α ≃ᵢ ↑(Set.range f)An isometry induces an isometric isomorphism between the source space and the range of the isometry.
- Defined in
- Mathlib.Topology.MetricSpace.Isometry
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 150 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- Equivproof · cited by 8,337
- Set.Elemstatement and proof · cited by 7,166
- Set.rangestatement and proof · cited by 4,705
- PseudoEMetricSpacestatement and proof · cited by 1,536
- EMetricSpacestatement and proof · cited by 242
- Isometrystatement and proof · cited by 230
- IsometryEquivstatement · cited by 177
- Equiv.ofInjectiveproof · cited by 64
- Isometry.injectiveproof · cited by 11
Cited by4
Results whose statement or proof uses this declaration.
- GromovHausdorff.eq_toGHSpace_iffproof · cited by 3
- Isometry.isometryEquivOnRange_applystatement and proof · cited by 0
- Isometry.isometryEquivOnRange_toEquivstatement and proof · cited by 0
- GromovHausdorff.toGHSpace_eq_toGHSpace_iff_isometryEquivproof · cited by 0