Sequentially_Compact_Metric_Subspace_Closed_iff_Compact_in_Itself
Provedmetric-spacesproofwikisequentially-compact-spaces
Let M be a metric space. Let C be a subspace of M which is sequentially compact in M. Then C is sequentially compact in itself iff C is closed in M.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Sequentially_Compact_Metric_Subspace_Closed_iff_Compact_in_Itself {X : Type _} [MetricSpace X] {C : Set X} (hC : IsCompact C) : IsClosed C := by sorrySource