Compact_First_Countable_Space_is_Sequentially_Compact

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

compact-spacesfirst-countable-spacesproofwikisequences

Let $T = \struct {S, \tau}$ be a compact first-countable topological space. Then every infinite sequence in $S$ has a convergent subsequence; that is, $T$ is sequentially compact.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Compact_First_Countable_Space_is_Sequentially_Compact {α : Type _} [TopologicalSpace α] [FirstCountableTopology α] [CompactSpace α] (f : ℕ → α) : ∃ x, ∃ φ : ℕ → ℕ, StrictMono φ ∧ Filter.Tendsto (f ∘ φ) Filter.atTop (nhds x) := by sorry

Source

https://proofwiki.org/wiki/Compact_First-Countable_Space_is_Sequentially_Compact

View graph