Sequentially_Compact_Metric_Space_is_Compact
Provedcompact-spacesmetric-spacesproofwikisequentially-compact-metric-space-is-compactsequentially-compact-spaces
A sequentially compact metric space is compact.
Preamble
import Mathlib.Topology.MetricSpace.Basic
Formal statement
theorem Sequentially_Compact_Metric_Space_is_Compact {α : Type _} [PseudoMetricSpace α] (h : ∀ (f : ℕ → α), ∃ (a : α) (φ : ℕ → ℕ), StrictMono φ ∧ Filter.Tendsto (f ∘ φ) Filter.atTop (nhds a)) : CompactSpace α := by sorrySource