Theorems · Inductive type · general topology
T2Space
(X : Type u) → [TopologicalSpace X] → Prop
A T₂ space, also known as a Hausdorff space, is one in which for every
x ≠ y there exists disjoint open sets around x and y. This is
the most widely used of the separation axioms.
- Defined in
- Mathlib.Topology.Separation.Hausdorff
- Cited by
- 1,351 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 2 definitions · 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 by1,458
Results whose statement or proof uses this declaration.
- HasSum.tsum_eqstatement and proof · cited by 150
- MeasureTheory.VectorMeasure.variationstatement and proof · cited by 125
- tendsto_nhds_uniquestatement and proof · cited by 118
- HasFDerivAt.fderivstatement and proof · cited by 93
- IsCompact.isClosedstatement and proof · cited by 77
- isClosed_eqstatement and proof · cited by 71
- HasFDerivWithinAt.fderivWithinstatement and proof · cited by 69
- HasProd.tprod_eqstatement and proof · cited by 49
- LinearMap.toContinuousLinearMapstatement and proof · cited by 43
- Topology.RelCWComplex.skeletonLTstatement and proof · cited by 34
- FiniteDimensional.completestatement and proof · cited by 29
- Topology.RelCWComplex.skeletonstatement and proof · cited by 28
Showing the 200 most cited of 1,458.