Theorems · Theorem · general topology
T1Space.t1
∀ {X : Type u} {inst : TopologicalSpace X} [self : T1Space X] (x : X), IsClosed {x}A singleton in a T₁ space is a closed set.
- Defined in
- Mathlib.Topology.Separation.Basic
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 4 from the axioms · uses no axioms
- Assumes
- T1Space
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- TopologicalSpacestatement and proof · cited by 24,529
- IsClosedstatement · cited by 1,639
- T1Spacestatement and proof · cited by 275
Cited by11
Results whose statement or proof uses this declaration.
- isClosed_singletonproof · cited by 66
- t1Space_TFAEproof · cited by 8
- PrimeSpectrum.t1Space_iff_isFieldproof · cited by 2
- exists_idempotent_of_compact_t2_of_continuous_add_leftproof · cited by 2
- exists_idempotent_of_compact_t2_of_continuous_mul_leftproof · cited by 2
- NormedAddGroupHom.isClosed_kerproof · cited by 1
- exists_compact_surjective_zorn_subsetproof · cited by 1
- CompactT2.Projective.extremallyDisconnectedproof · cited by 1
- t1Space_antitoneproof · cited by 1
- Distribution.dsupport_deltaproof · cited by 0
- Distribution.TemperedDistribution.dsupport_deltaproof · cited by 0