Theorems · Theorem · general topology

IsCountablyCompact.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

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.

Defined in

Mathlib.Topology.Compactness.CountablyCompact

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpace