Theorems · Inductive type · general topology
CompletelyRegularSpace
(X : Type u) → [TopologicalSpace X] → Prop
A space is completely regular if points can be separated from closed sets via continuous functions to the unit interval.
- Cited by
- 23 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- TopologicalSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement · cited by 24,529
Cited by28
Results whose statement or proof uses this declaration.
- CompletelyRegularSpace.completely_regularstatement and proof · cited by 4
- isInducing_stoneCechUnitstatement and proof · cited by 4
- CompletelyRegularSpace.completely_regular_isOpenstatement and proof · cited by 3
- completelyRegularSpace_iff_isOpenstatement and proof · cited by 2
- Topology.IsInducing.completelyRegularSpacestatement and proof · cited by 2
- T35Space.casesOnstatement and proof · cited by 1
- MeasureTheory.diracProbaHomeomorphstatement and proof · cited by 1
- MeasureTheory.tendsto_diracProbaEquivSymm_iff_tendstostatement and proof · cited by 1
- MeasureTheory.tendsto_diracProba_iff_tendstostatement and proof · cited by 1
- isDenseInducing_stoneCechUnitstatement and proof · cited by 1
- CompletelyRegularSpace.casesOnstatement and proof · cited by 1
- CompletelyRegularSpace.exists_BCNNstatement and proof · cited by 1