Heine_Borel_Theorem_Real_Line
Provedcompactnessproofwikireal-analysistopology
A subset C of R is compact iff it is closed and bounded.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic import Mathlib.Topology.MetricSpace.Basic theorem Heine_Borel_Theorem_Real_Line (C : Set ℝ) : IsCompact C ↔ IsClosed C ∧ Bornology.IsBounded C := by sorry
Source