Theorems · Definition · general topology
IsCountablyCompact
{E : Type u_2} → [TopologicalSpace E] → Set E → PropA set A is countably compact if every countably generated proper filter f with
f ≤ 𝓟 A has a cluster point in A.
- Cited by
- 33 results in Mathlib
- Foundations
- Depth 49 from the axioms · uses propext, Quot.sound
- Assumes
- TopologicalSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · 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
- ClusterPtproof · cited by 138
Cited by35
Results whose statement or proof uses this declaration.
- CountablyCompactSpace.isCountablyCompact_univstatement · cited by 3
- IsCountablyCompact.of_seq_clusterPtstatement · cited by 3
- isCountablyCompact_iff_seq_clusterPtstatement and proof · cited by 2
- IsCountablyCompact.elim_finite_subcoverstatement and proof · cited by 2
- IsLindelof.isCompactstatement and proof · cited by 2
- isCountablyCompact_iff_countable_open_coverstatement and proof · cited by 1
- isCountablyCompact_iff_countable_open_cover'statement · cited by 1
- isCountablyCompact_iff_countablyCompactSpacestatement · cited by 1
- isCountablyCompact_iff_isCountablyCompact_univstatement and proof · cited by 1
- isCountablyCompact_univ_iffstatement and proof · cited by 1
- IsSeqCompact.isCountablyCompactstatement · cited by 1
- Topology.IsEmbedding.isCountablyCompact_iffstatement · cited by 1