Theorems · Theorem · general topology
Isometry.isClosedEmbedding
∀ {α : Type u} {γ : Type w} [inst : EMetricSpace α] [CompleteSpace α] [inst_2 : EMetricSpace γ] {f : α → γ},
Isometry f → Topology.IsClosedEmbedding fAn isometry from a complete emetric space is a closed embedding
- Defined in
- Mathlib.Topology.MetricSpace.Isometry
- Cited by
- 15 results in Mathlib
- Foundations
- Depth 153 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CompleteSpacestatement and proof · cited by 2,532
- EMetricSpacestatement and proof · cited by 242
- Isometrystatement and proof · cited by 230
- Topology.IsClosedEmbeddingstatement · cited by 195
- LipschitzWith.uniformContinuousproof · cited by 33
- Isometry.lipschitzproof · cited by 22
- Isometry.antilipschitzproof · cited by 14
- AntilipschitzWith.isClosedEmbeddingproof · cited by 3
Cited by15
Results whose statement or proof uses this declaration.
- cfc_real_eq_complexproof · cited by 4
- cfcₙ_real_eq_complexproof · cited by 3
- Complex.isClosedEmbedding_intCastproof · cited by 2
- Real.isClosedEmbedding_intCastproof · cited by 2
- NumberField.InfinitePlace.Completion.isClosed_image_extensionEmbeddingproof · cited by 1
- MeasureTheory.hasDerivAt_resolventTransformproof · cited by 1
- gelfandTransform_bijectiveproof · cited by 1
- MeasureTheory.norm_resolvent_le_inv_infDist_supportproof · cited by 1
- CStarAlgebra.isClosed_nonnegproof · cited by 0
- QuasispectrumRestricts.isometric_cfcproof · cited by 0
- SpectrumRestricts.isometric_cfcproof · cited by 0