Theorems · Theorem · general topology
isLindelof_empty
∀ {X : Type u} [inst : TopologicalSpace X], IsLindelof ∅The empty set is a Lindelof set.
- Defined in
- Mathlib.Topology.Compactness.Lindelof
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 52 from the axioms · uses propext, Quot.sound
- Assumes
- TopologicalSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
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
- Filterproof · cited by 8,121
- Filter.NeBotproof · cited by 853
- Filter.principalproof · cited by 740
- Filter.le_principal_iffproof · cited by 87
- IsLindelofstatement · cited by 85
- CountableInterFilterproof · cited by 78
- Filter.empty_mem_iff_botproof · cited by 18
- Filter.NeBot.neproof · cited by 17
Cited by3
Results whose statement or proof uses this declaration.
- hasBasis_coLindelofproof · cited by 5
- hasBasis_coclosedLindelofproof · cited by 2
- Set.Subsingleton.isLindelofproof · cited by 0