Sequentially_Compact_Metric_Space_is_Lindel_f
Provedlindel-f-spacesmetric-spacesproofwikisequentially-compact-spaces
Let be a metric space. Let be sequentially compact. Then is also a Lindelöf space. That is, from every open cover of , it is possible to extract a countable subcover.
Preamble
import Mathlib.Topology.MetricSpace.Basic
Formal statement
theorem Sequentially_Compact_Metric_Space_is_Lindel_f {α : Type _} [MetricSpace α] [CompactSpace α] : TopologicalSpace.SeparableSpace α := by sorrySource