Existing in Mathlib · Topology
Heine–Borel Theorem
In a proper Hausdorff (pseudo-)metric space, a set is compact exactly when it is both closed and bounded.
- compactness
- closed sets
- bounded sets
- proper metric spaces
- Hausdorff separation
- closed balls
Exact theorem
Exact Mathlib statement
theorem Metric.isCompact_iff_isClosed_bounded {α : Type*} [PseudoMetricSpace α] {s : Set α} [T2Space α] [ProperSpace α] : IsCompact s ↔ IsClosed s ∧ IsBounded sThe theorem at a glance
Heine–Borel theorem at a glance
A visual guide to the theorem's hypotheses, structure, and conclusion; the exact statement gives the formal detail.
Heine–Borel theorem at a glance
Detailed visual description
The poster foregrounds [PseudoMetricSpace α], [T2Space α], and [ProperSpace α] together with IsCompact s ↔ IsClosed s ∧ IsBounded s. A sealed bounded set and the same set inside a compact closed ball illustrate the two directions. The lower route explains that compact sets are closed and bounded, while a closed bounded set lies in a compact closed ball and is therefore compact. The exact-scope footer excludes an arbitrary-metric-space reading and notes that finite dimensionality and local compactness are not separate hypotheses of this declaration.
Statement structure
From hypotheses to conclusion
This map summarizes the statement's structure; the exact Mathlib declaration remains authoritative.
One set across compact, closed, bounded, and compact-ball views
Detailed visual description
One vector-defined irregular set is reused without redrawing in four views. Seven dashed cobalt neighborhoods cover it at left. The upper central occurrence has a sealed rust boundary, while the lower central occurrence lies inside a finite-radius dotted cobalt ring; an emerald brace groups these two properties. At right, the same set lies strictly inside a double antique-gold closed ball with a finite lattice. An upper emerald arrow travels left-to-right and a lower emerald arrow returns right-to-left, encoding the equivalence.
Why it matters
A mathematical landmark
Heine–Borel is a central bridge between topology and metric geometry. Mathlib's selected form isolates the structural reason the closed-and-bounded criterion works: properness supplies compact closed balls, while Hausdorff separation supplies closedness of compact sets.
ProofAtlas record
What has been checked
Mathlib is the source of the theorem; the local Lean replay and page review are separate.
Claim boundary
No new theorem is claimed
This page indexes Mathlib's proper-space Heine–Borel declaration: for [PseudoMetricSpace α], [T2Space α], [ProperSpace α], and s : Set α, IsCompact s is equivalent to IsClosed s ∧ IsBounded s. It is not a closed-and-bounded criterion for arbitrary metric spaces. The selected declaration does not separately assume finite dimensionality or a LocalCompactSpace instance.
- The selected declaration requires [T2Space α] and [ProperSpace α] in addition to the ambient [PseudoMetricSpace α]; it is not stated for every metric space.
- The declaration does not say that closedness alone or boundedness alone implies compactness.
- Finite-dimensional Euclidean and normed-space forms are familiar special contexts, but finite dimensionality is not a hypothesis of this selected declaration.
- The selected declaration does not separately assume a LocalCompactSpace instance or state an equivalence between properness and local compactness.
- ProofAtlas is indexing an existing Mathlib theorem, and generated explanations and visuals are not proof evidence.
Source and local evidence
Where the theorem comes from
- Existing declaration
Metric.isCompact_iff_isClosed_boundedin mathlib- Relationship
- The checked artifact is the upstream declaration itself
- Local Lean evidence
artifact.library.mathlib.heine-borel-theorem.v001