Theorems · Inductive type · general topology
LindelofSpace
(X : Type u_2) → [TopologicalSpace X] → Prop
X is a Lindelöf space iff every open cover has a countable subcover.
- Defined in
- Mathlib.Topology.Compactness.Lindelof
- Cited by
- 24 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 by26
Results whose statement or proof uses this declaration.
- isLindelof_univstatement and proof · cited by 6
- LindelofSpace.isLindelof_univstatement and proof · cited by 4
- isLindelof_iff_lindelofSpacestatement · cited by 2
- isLindelof_univ_iffstatement and proof · cited by 2
- IsClosed.isLindelofstatement and proof · cited by 2
- isLindelof_rangestatement and proof · cited by 1
- countable_cover_nhds_interiorstatement and proof · cited by 1
- countable_of_Lindelof_of_discretestatement and proof · cited by 1
- LindelofSpace.compactSpacestatement and proof · cited by 1
- isLindelof_diagonalstatement and proof · cited by 0
- isLindelof_iff_LindelofSpacestatement · cited by 0
- lindelofSpace_of_countable_subfamily_closedstatement · cited by 0