Theorems · Theorem · general topology
isCountablyCompact_empty
∀ {E : Type u_2} [inst : TopologicalSpace E], IsCountablyCompact ∅The empty set is countably compact.
- Cited by
- 1 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.IsCountablyGeneratedproof · cited by 220
- Filter.le_principal_iffproof · cited by 87
- IsCountablyCompactstatement · cited by 33
- Filter.empty_mem_iff_botproof · cited by 18
- Filter.NeBot.ne'proof · cited by 7
Cited by1
Results whose statement or proof uses this declaration.
- Finset.isCountablyCompact_biUnionproof · cited by 1