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
Statement and scope
Read the exact Mathlib declaration
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