Theorems · Definition · general topology
UniformSpace.hausdorff
(α : Type u_1) → [UniformSpace α] → UniformSpace (Set α)
The Hausdorff uniformity on the powerset of a uniform space. Used for defining the uniformities
on Closeds, Compacts and NonemptyCompacts.
See note [reducible non-instances].
- Defined in
- Mathlib.Topology.UniformSpace.Closeds
- Cited by
- 33 results in Mathlib
- Foundations
- Depth 68 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- UniformSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- UniformSpacestatement and proof · cited by 2,040
- uniformityproof · cited by 765
- Filter.lift'proof · cited by 99
- hausdorffEntourageproof · cited by 35
- UniformSpace.ofCoreproof · cited by 1
Cited by34
Results whose statement or proof uses this declaration.
- Filter.HasBasis.uniformity_hausdorffstatement · cited by 8
- TopologicalSpace.Compacts.isUniformEmbedding_coestatement · cited by 7
- TopologicalSpace.NonemptyCompacts.isUniformEmbedding_coestatement · cited by 7
- TopologicalSpace.Closeds.isUniformEmbedding_coestatement · cited by 6
- TopologicalSpace.Closeds.uniformContinuous_coestatement · cited by 5
- TopologicalSpace.NonemptyCompacts.uniformContinuous_coestatement · cited by 4
- TopologicalSpace.Compacts.uniformContinuous_coestatement · cited by 4
- UniformSpace.hausdorff.isOpen_inter_nonempty_of_isOpenstatement · cited by 4
- UniformSpace.hausdorff.isUniformEmbedding_singletonstatement · cited by 4
- TotallyBounded.powerset_hausdorffstatement · cited by 3
- IsUniformInducing.image_hausdorffstatement · cited by 3
- UniformSpace.hausdorff.uniformContinuous_prodstatement · cited by 3