Theorems · Theorem · general topology

isCountablyCompact_iff_seq_clusterPt

∀ {E : Type u_2} [inst : 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.

Defined in

Mathlib.Topology.Compactness.CountablyCompact

Cited by

2 results in Mathlib

Foundations

Depth 71 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpace