Theorems · Theorem · general topology
Isometry.continuous
∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β},
Isometry f → Continuous fAn isometry is continuous.
- Defined in
- Mathlib.Topology.MetricSpace.Isometry
- Cited by
- 23 results in Mathlib
- Foundations
- Depth 151 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Continuousstatement · cited by 2,592
- PseudoEMetricSpacestatement and proof · cited by 1,536
- Isometrystatement and proof · cited by 230
- LipschitzWith.continuousproof · cited by 30
- Isometry.lipschitzproof · cited by 22
Cited by23
Results whose statement or proof uses this declaration.
- LinearIsometryEquiv.continuousproof · cited by 14
- LinearIsometry.continuousproof · cited by 4
- upperHemicontinuous_quasispectrumproof · cited by 3
- GromovHausdorff.ghDist_le_hausdorffDistproof · cited by 3
- AffineIsometryEquiv.continuousproof · cited by 3
- Isometry.map_hausdorffMeasureproof · cited by 2
- NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal_applyproof · cited by 2
- Unitization.continuous_inrproof · cited by 2
- NumberField.InfinitePlace.Completion.liesOver_extensionEmbeddingproof · cited by 2
- IsometryEquiv.continuousproof · cited by 2
- HasDerivAt.comp_semilinearproof · cited by 2
- Isometry.extensionHom_coeproof · cited by 2