Countably compact sets

A set A in a topological space is countably compact if every countably generated proper filter contained in A has a cluster point in A. Equivalently, every sequence in A has a cluster point in A, and every countable open cover of A admits a finite subcover.

Main definitions

• IsCountablyCompact A: A is countably compact (every countably generated proper filter contained in A has a cluster point in A).
• CountablyCompactSpace E: the whole space E is countably compact.

Main results

• IsCountablyCompact.elim_directed_cover: for every countable open directed cover of a countably compact set, some single element of the cover contains the set.
• IsCountablyCompact.elim_finite_subcover: a countably compact set has a finite subcover for any countable open cover.
• isCountablyCompact_iff_countable_open_cover: countable compactness is equivalent to the finite subcover property for countable covers.
• IsCompact.isCountablyCompact: compact sets are countably compact.
• IsSeqCompact.isCountablyCompact: sequentially compact sets are countably compact.
• IsCountablyCompact.isSeqCompact: in a first-countable space, countable compactness implies sequential compactness.
• IsCountablyCompact.exists_accPt_of_infinite: every infinite subset of a countably compact set has an accumulation point in the set.
• isCountablyCompact_iff_infinite_subset_has_accPt: in a T₁ space, countable compactness is equivalent to the Bolzano–Weierstrass property (every infinite subset has an accumulation point).
• IsLindelof.isCompact: a countably compact Lindelöf set is compact.
• IsCountablyCompact.image: the continuous image of a countably compact set is countably compact.

References

• [Engelking, General Topology][engelking1989]

def IsCountablyCompact {E : Type u_2} [TopologicalSpace E] (A : Set E) : Prop

A set A is countably compact if every countably generated proper filter f with f ≤ 𝓟 A has a cluster point in A.

class CountablyCompactSpace (E : Type u_4) [TopologicalSpace E] : Prop

A topological space is countably compact if every countably generated proper filter has a cluster point.

• isCountablyCompact_univ : IsCountablyCompact Set.univ

theorem isCountablyCompact_empty {E : Type u_2} [TopologicalSpace E] : IsCountablyCompact ∅

The empty set is countably compact.

theorem isCountablyCompact_singleton {E : Type u_2} [TopologicalSpace E] {x : E} : IsCountablyCompact {x}

A singleton set is countably compact.

theorem IsCountablyCompact.of_isClosed_subset {E : Type u_2} [TopologicalSpace E] {A B : Set E} (hA : IsCountablyCompact A) (hB : IsClosed B) (hBA : B ⊆ A) : IsCountablyCompact B

A closed subset of a countably compact set is countably compact.

theorem isCountablyCompact_iff_seq_clusterPt {E : Type u_2} [TopologicalSpace E] {A : Set E} : IsCountablyCompact A ↔ ∀ (x : ℕ → E), (∀ᶠ (n : ℕ) in Filter.atTop, x n ∈ A) → ∃ a ∈ A, MapClusterPt a Filter.atTop x

A set is countably compact if and only if every sequence eventually in it has a cluster point in it.

theorem IsCountablyCompact.seq_clusterPt {E : Type u_2} [TopologicalSpace E] {A : Set E} : IsCountablyCompact A → ∀ (x : ℕ → E), (∀ᶠ (n : ℕ) in Filter.atTop, x n ∈ A) → ∃ a ∈ A, MapClusterPt a Filter.atTop x

Alias of the forward direction of isCountablyCompact_iff_seq_clusterPt.

---

A set is countably compact if and only if every sequence eventually in it has a cluster point in it.

theorem IsCountablyCompact.of_seq_clusterPt {E : Type u_2} [TopologicalSpace E] {A : Set E} : (∀ (x : ℕ → E), (∀ᶠ (n : ℕ) in Filter.atTop, x n ∈ A) → ∃ a ∈ A, MapClusterPt a Filter.atTop x) → IsCountablyCompact A

Alias of the reverse direction of isCountablyCompact_iff_seq_clusterPt.

---

A set is countably compact if and only if every sequence eventually in it has a cluster point in it.

theorem IsCountablyCompact.elim_directed_cover {ι : Type u_1} {E : Type u_2} [TopologicalSpace E] {A : Set E} [Countable ι] [Nonempty ι] (hA : IsCountablyCompact A) (U : ι → Set E) (hUo : ∀ (i : ι), IsOpen (U i)) (hAU : A ⊆ ⋃ (i : ι), U i) (hdU : Directed (fun (x1 x2 : Set E) => x1 ⊆ x2) U) : ∃ (i : ι), A ⊆ U i

For every countable open directed cover of a countably compact set, there exists a single element of the cover which itself includes the set.

theorem IsCountablyCompact.elim_finite_subcover {ι : Type u_1} {E : Type u_2} [TopologicalSpace E] {A : Set E} (hA : IsCountablyCompact A) [Countable ι] {U : ι → Set E} (hUo : ∀ (i : ι), IsOpen (U i)) (hAU : A ⊆ ⋃ (i : ι), U i) : ∃ (t : Finset ι), A ⊆ ⋃ i ∈ t, U i

A countably compact set has a finite subcover for any countable open cover.

theorem isCountablyCompact_iff_countable_open_cover {E : Type u_2} [TopologicalSpace E] {A : Set E} : IsCountablyCompact A ↔ ∀ (U : ℕ → Set E), (∀ (i : ℕ), IsOpen (U i)) → A ⊆ ⋃ (i : ℕ), U i → ∃ (t : Finset ℕ), A ⊆ ⋃ i ∈ t, U i

A set is countably compact if and only if every countable open cover has a finite subcover.

theorem IsCountablyCompact.elim_finite_subcover_image {ι : Type u_1} {E : Type u_2} [TopologicalSpace E] {A : Set E} (hA : IsCountablyCompact A) {b : Set ι} (hb : b.Countable) {U : ι → Set E} (hUo : ∀ i ∈ b, IsOpen (U i)) (hAU : A ⊆ ⋃ i ∈ b, U i) : ∃ t ⊆ b, t.Finite ∧ A ⊆ ⋃ i ∈ t, U i

A countably compact set has a finite subcover for any countable open cover indexed by a subset.

theorem isCountablyCompact_iff_countable_open_cover' {E : Type u_2} [TopologicalSpace E] {A : Set E} : IsCountablyCompact A ↔ ∀ (U : ℕ → Set E), (∀ (i : ℕ), IsOpen (U i)) → A ⊆ ⋃ (i : ℕ), U i → ∃ (t : Set ℕ), t.Finite ∧ A ⊆ ⋃ i ∈ t, U i

Variant of isCountablyCompact_iff_countable_open_cover with Set ℕ instead of Finset ℕ.

theorem IsCompact.isCountablyCompact {E : Type u_2} [TopologicalSpace E] {A : Set E} (hA : IsCompact A) : IsCountablyCompact A

A compact set is countably compact.

instance CompactSpace.CountablyCompactSpace {X : Type u_4} [TopologicalSpace X] [CompactSpace X] : _root_.CountablyCompactSpace X

A compact space is countably compact.

theorem IsSeqCompact.isCountablyCompact {E : Type u_2} [TopologicalSpace E] {A : Set E} (hA : IsSeqCompact A) : IsCountablyCompact A

A sequentially compact set is countably compact.

instance SeqCompactSpace.CountablyCompactSpace {X : Type u_4} [TopologicalSpace X] [SeqCompactSpace X] : _root_.CountablyCompactSpace X

A sequentially compact space is countably compact.

theorem IsCountablyCompact.isSeqCompact {E : Type u_2} [TopologicalSpace E] {A : Set E} [FirstCountableTopology E] (hA : IsCountablyCompact A) : IsSeqCompact A

In a first-countable space, a countably compact set is sequentially compact.

instance CountablyCompactSpace.SeqCompactSpace {X : Type u_4} [TopologicalSpace X] [FirstCountableTopology X] [CountablyCompactSpace X] : _root_.SeqCompactSpace X

In a first-countable countably compact space is sequentially compact.

theorem isCountablyCompact_iff_isSeqCompact {E : Type u_2} [TopologicalSpace E] {A : Set E} [FirstCountableTopology E] : IsCountablyCompact A ↔ IsSeqCompact A

In a first-countable space, a set is countably compact iff it is sequentially compact.

theorem IsCountablyCompact.exists_accPt_of_infinite {E : Type u_2} [TopologicalSpace E] {A B : Set E} (hA : IsCountablyCompact A) (hBA : B ⊆ A) (hB : B.Infinite) : ∃ a ∈ A, AccPt a (Filter.principal B)

Every infinite subset of a countably compact set has an accumulation point in the set.

theorem isCountablyCompact_iff_infinite_subset_has_accPt {E : Type u_2} [TopologicalSpace E] [T1Space E] {A : Set E} : IsCountablyCompact A ↔ ∀ B ⊆ A, B.Infinite → ∃ a ∈ A, AccPt a (Filter.principal B)

In a T₁ space, a set is countably compact if and only if every infinite subset has an accumulation point in the set.

theorem IsLindelof.isCompact {E : Type u_2} [TopologicalSpace E] {A : Set E} (hA : IsCountablyCompact A) (hl : IsLindelof A) : IsCompact A

A countably compact Lindelöf set is compact.

theorem LindelofSpace.CompactSpace {X : Type u_4} [TopologicalSpace X] [LindelofSpace X] [h : CountablyCompactSpace X] : _root_.CompactSpace X

A countably compact Lindelöf space is compact.

theorem IsCountablyCompact.isCompact {E : Type u_2} [TopologicalSpace E] {A : Set E} [HereditarilyLindelofSpace E] (hA : IsCountablyCompact A) : IsCompact A

In a Hereditarily Lindelöf space, a countably compact set is compact.

theorem IsCountablyCompact.image {E : Type u_2} {F : Type u_3} [TopologicalSpace E] [TopologicalSpace F] {A : Set E} (hA : IsCountablyCompact A) {f : E → F} (hf : Continuous f) : IsCountablyCompact (f '' A)

The continuous image of a countably compact set is countably compact.

theorem IsCountablyCompact.union {E : Type u_2} [TopologicalSpace E] {A B : Set E} (hA : IsCountablyCompact A) (hB : IsCountablyCompact B) : IsCountablyCompact (A ∪ B)

The union of two countably compact sets is countably compact.

theorem Finset.isCountablyCompact_biUnion {ι : Type u_1} {E : Type u_2} [TopologicalSpace E] (s : Finset ι) {f : ι → Set E} (hf : ∀ i ∈ s, IsCountablyCompact (f i)) : IsCountablyCompact (⋃ i ∈ s, f i)

A finite union of countably compact sets is countably compact.

theorem Set.Finite.isCountablyCompact_biUnion {ι : Type u_1} {E : Type u_2} [TopologicalSpace E] {s : Set ι} {f : ι → Set E} (hs : s.Finite) (hf : ∀ i ∈ s, IsCountablyCompact (f i)) : IsCountablyCompact (⋃ i ∈ s, f i)

A finite union of countably compact sets is countably compact.

theorem Set.Finite.isCountablyCompact_sUnion {E : Type u_2} [TopologicalSpace E] {S : Set (Set E)} (hf : S.Finite) (hc : ∀ s ∈ S, IsCountablyCompact s) : IsCountablyCompact (⋃₀ S)

A finite union of countably compact sets is countably compact.

theorem isCountablyCompact_iUnion {E : Type u_2} [TopologicalSpace E] {ι : Sort u_4} {f : ι → Set E} [Finite ι] (h : ∀ (i : ι), IsCountablyCompact (f i)) : IsCountablyCompact (⋃ (i : ι), f i)

A finite union of countably compact sets is countably compact.