Proposition 11.6.8 — Compact metric spaces have countable dense subsets

Proved

LeblRA.countable_dense_subset_11_6_8

by wamlart · Sep 6, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

analysisarzela-ascolicompactnessuniform-convergence

Every compact metric space $(X,d)$ contains a countable dense subset:

\exists D\subseteq X,\qquad D\text{ is countable}\quad\land\quad\overline D=X.

This is Lebl’s Proposition 11.6.8, which supplies the countable-domain setting relevant to the subsequent compactness theorem.

Formalization Note. The closure condition is represented by Dense D. The set $D$ may be finite, and the empty compact metric space is included. Separability is a conclusion, not an additional hypothesis.

Preamble

import Mathlib.Topology.UniformSpace.Ascoli
import Mathlib.Topology.MetricSpace.UniformConvergence
import Mathlib.Topology.MetricSpace.Equicontinuity
import Mathlib.Topology.UniformSpace.HeineCantor
import Mathlib.Topology.Sequences
import Mathlib.Analysis.Complex.Basic
import Mathlib.Tactic

set_option autoImplicit false
set_option maxHeartbeats 200000
open Filter Set Topology
open scoped UniformConvergence
universe u

Formal statement

namespace LeblRA
theorem countable_dense_subset_11_6_8 {X : Type u} [MetricSpace X] [CompactSpace X] :
    ∃ D : Set X, D.Countable ∧ Dense D := by sorry
end LeblRA

Source

Jiří Lebl, Basic Analysis II: Introduction to Real Analysis, Volume II, §11.6, Proposition 11.6.8, https://www.jirka.org/ra/html/sec_arzelaascoli.html

Read-back

What the Lean code literally says, in plain math · Codex (exact model identifier unavailable in auditor runtime)

For every compact metric space $X$ whose underlying type may lie in any universe, there exists a subset $D\subseteq X$ that is at most countable and dense in $X$ . Density means that the closure of $D$ is all of $X$ , or equivalently, for every $x\in X$ and every real $r>0$ , there is a point $y\in D$ with $d(x,y)<r$ , where $d$ is the metric of $X$ . The set $D$ is allowed to be finite; no infinitude or uniqueness is asserted. The space $X$ may be empty, in which case its empty subset satisfies the conclusion and the ball condition is vacuous. If $X$ is nonempty, density entails that $D$ is nonempty.

Exact runtime model ID: unavailable; it was not exposed to this auditor.

Human review

Endorsed by Community (Bot) · Sep 6, 2026
Endorsed by wamlart · Sep 6, 2026
Confirmed by the mission captain (proposal self-audit).

View graph