Heine–Borel Theorem

Statement

A subset $K \subseteq \mathbb{R}^n$ is compact if and only if it is closed and bounded:

Compactness means every open cover admits a finite subcover. Closed means the set contains all its limit points. Bounded means it fits inside some ball $B_r(0)$.

Visualization

Consider $\mathbb{R}^1$. Below, a closed bounded set $[1,3]$ versus the open unbounded ray $(0,\infty)$.

Number line:
──0────[1═══3]────────5──────────────▶
       ↑     ↑
    closed  closed
    bounded bounded
    compact!

──0════(0═══════════════════════════▶
        ↑
   open, unbounded, not compact
   The cover {(−1, n) : n ∈ ℕ} has no finite subcover.

The set $[1,3]$ can be covered by finitely many open intervals no matter how you choose them — any open cover must include intervals that together blanket $[1,3]$, and compactness guarantees a finite selection suffices.

For an open set $(1,3)$: the cover $\{(1+\tfrac{1}{n}, 3) : n \ge 1\}$ is an open cover with no finite subcover (every finite sub-collection misses points near $1$).

Proof Sketch

Compact $\Rightarrow$ closed and bounded. A compact subset of a Hausdorff space is closed. If $K$ were unbounded, the open cover $\{B_n(0) : n \in \mathbb{N}\}$ would have no finite subcover — contradiction.

Closed and bounded $\Rightarrow$ compact. A closed bounded set sits inside some $[-R,R]^n$. The box $[-R,R]^n$ is a finite product of compact intervals, hence compact by Tychonoff's TheoremTychonoff's Theorem$$\prod_{i \in I} X_i \text{ compact} \iff \forall i,\; X_i \text{ compact}$$An arbitrary product of compact spaces is compact in the product topologyRead more →. A closed subset of a compact set is compact.

Connections

Heine–Borel is the foundation for a cascade of classical theorems:

• Bolzano–Weierstrass TheoremBolzano–Weierstrass Theorem$$\text{bounded } (x_n) \subseteq \mathbb{R}^n \implies \exists\, \text{convergent subsequence}$$Every bounded sequence in ℝⁿ has a convergent subsequenceRead more → — a bounded sequence in $\mathbb{R}^n$ has a convergent subsequence; the compact enclosing box does the work.
• Brouwer Fixed-Point TheoremBrouwer Fixed-Point Theorem$$f : D^n \to D^n \text{ continuous} \implies \exists\, x,\; f(x) = x$$Every continuous map from a compact convex set to itself has a fixed pointRead more → — the closed unit ball is compact (closed and bounded), enabling degree-theory and homological arguments.
• Tychonoff's TheoremTychonoff's Theorem$$\prod_{i \in I} X_i \text{ compact} \iff \forall i,\; X_i \text{ compact}$$An arbitrary product of compact spaces is compact in the product topologyRead more → — the infinite-dimensional generalisation: arbitrary products of compact spaces are compact. Heine–Borel is the $n=1$ finite-dimensional case.
• Hausdorff DistanceHausdorff Distance$$d_H(A, B) = \max\left(\sup_{a \in A} d(a, B),\ \sup_{b \in B} d(b, A)\right)$$A metric on non-empty compact sets, foundation for the IFS attractor theoremRead more → — the space of non-empty compact subsets of $\mathbb{R}^n$ is itself complete and compact under the Hausdorff metric, making IFS attractors well-defined.
• Urysohn's LemmaUrysohn's Lemma$$\exists\, f : X \to [0,1],\quad f|_s = 0,\; f|_t = 1$$In a normal space, disjoint closed sets can be separated by a continuous functionRead more → — compact Hausdorff spaces are normal, so Urysohn's construction applies.
• Iterated Function SystemsIterated Function Systems$$A = \bigcup_{i=1}^{N} f_i(A)$$Constructing fractals via contractive affine transformationsRead more → — the Hutchinson operator acts on $\mathcal{K}^*(\mathbb{R}^n)$; Heine–Borel guarantees that iterates stay in a compact ambient space.

import Mathlib.Topology.MetricSpace.Bounded
import Mathlib.Analysis.InnerProductSpace.EuclideanDist

open Bornology

/-- **Heine–Borel theorem** for Euclidean space ℝⁿ.
    Mathlib: `isCompact_iff_isClosed_bounded` in `ProperSpace` instances. -/
theorem heine_borel {n : ℕ} {s : Set (EuclideanSpace ℝ (Fin n))} :
    IsCompact s ↔ IsClosed s ∧ IsBounded s :=
  isCompact_iff_isClosed_bounded