Theorems · Definition · general topology
NonemptyCompacts.kuratowskiEmbedding
(α : Type u) → [inst : MetricSpace α] → [CompactSpace α] → [Nonempty α] → TopologicalSpace.NonemptyCompacts ↥(lp (fun x => ℝ) ⊤)
Version of the Kuratowski embedding for nonempty compacts
- Defined in
- Mathlib.Topology.MetricSpace.Kuratowski
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 237 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement · cited by 25,697
- ENNRealstatement · cited by 9,879
- Top.topstatement · cited by 9,680
- Set.rangeproof · cited by 4,705
- AddSubgroupstatement · cited by 3,232
- MetricSpacestatement and proof · cited by 1,684
- CompactSpacestatement and proof · cited by 593
- PreLpstatement · cited by 163
- lpstatement · cited by 157
- TopologicalSpace.NonemptyCompactsstatement · cited by 137
- kuratowskiEmbeddingproof · cited by 5
Cited by5
Results whose statement or proof uses this declaration.
- GromovHausdorff.toGHSpaceproof · cited by 8
- GromovHausdorff.eq_toGHSpace_iffproof · cited by 3
- GromovHausdorff.hausdorffDist_optimalproof · cited by 1
- NonemptyCompacts.kuratowskiEmbedding.congr_simpstatement and proof · cited by 0
- GromovHausdorff.toGHSpace_eq_toGHSpace_iff_isometryEquivproof · cited by 0