Theorem 11.6.9 — Arzelà–Ascoli theorem

Proved

LeblRA.arzela_ascoli_11_6_9

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

analysisarzela-ascolicompactnessuniform-convergence

Let $(X,d)$ be a compact metric space and let $F_n:X\to\mathbb C$ be continuous functions. Suppose that

\forall x\in X\;\exists M_x\in\mathbb R\;\forall n\in\mathbb N,\qquad |F_n(x)|\le M_x,

and that

\forall\varepsilon>0\;\exists\delta>0\;\forall x,y\in X\;\forall n\in\mathbb N,\qquad d(x,y)<\delta\Longrightarrow |F_n(x)-F_n(y)|<\varepsilon.

Then the sequence is uniformly bounded:

\exists M\in\mathbb R\;\forall n\in\mathbb N\;\forall x\in X,\qquad |F_n(x)|\le M,

and there exist a strictly increasing map $\varphi:\mathbb N\to\mathbb N$ and a continuous function $f:X\to\mathbb C$ such that $F_{\varphi(n)}$ converges uniformly to $f$ . These are both conclusions of Lebl’s Theorem 11.6.9, Arzelà–Ascoli.

Formalization Note. Uniform boundedness is proved, not assumed. The subsequence index satisfies StrictMono; convergence is TendstoUniformly. Continuity of the limit is explicit, consistent with uniform convergence of continuous functions. Empty compact metric domains are allowed.

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 arzela_ascoli_11_6_9 {X : Type u} [MetricSpace X] [CompactSpace X]
    (F : ℕ → X → ℂ) (hF : ∀ n, Continuous (F n))
    (hb : ∀ x, ∃ M : ℝ, ∀ n, ‖F n x‖ ≤ M)
    (he : ∀ ε > 0, ∃ δ > 0, ∀ x y, dist x y < δ → ∀ n, ‖F n x - F n y‖ < ε) :
    (∃ M : ℝ, ∀ n x, ‖F n x‖ ≤ M) ∧
    ∃ (φ : ℕ → ℕ) (f : X → ℂ), StrictMono φ ∧ Continuous f ∧
      TendstoUniformly (fun n => F (φ n)) f atTop := by sorry
end LeblRA

Source

Jiří Lebl, Basic Analysis II: Introduction to Real Analysis, Volume II, §11.6, Theorem 11.6.9, 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$ , with underlying type in any universe, and every sequence of functions $F_n:X\to\mathbb C$ indexed by all natural numbers including $0$ , assume that each $F_n$ is continuous; that for each $x\in X$ there exists a real number $M$ , allowed to depend on $x$ , such that $|F_n(x)|\le M$ for every natural number $n$ ; and that for every real $\varepsilon>0$ there exists a real $\delta>0$ such that $d(x,y)<\delta$ implies $|F_n(x)-F_n(y)|<\varepsilon$ for all $x,y\in X$ and all natural numbers $n$ , with this $\delta$ independent of the points and of $n$ . Then both of the following hold: there exists a single real number $M$ such that $|F_n(x)|\le M$ for every natural number $n$ and every $x\in X$ ; and there exist a strictly increasing function $\varphi:\mathbb N\to\mathbb N$ and a continuous function $f:X\to\mathbb C$ such that $F_{\varphi(n)}$ converges uniformly to $f$ . Strict increase means that $i<j$ implies $\varphi(i)<\varphi(j)$ , without a prescribed value at $0$ ; uniform convergence means that for every real $\eta>0$ there is a natural number $N$ such that $|F_{\varphi(n)}(x)-f(x)|<\eta$ for all $n\ge N$ and all $x\in X$ , with one $N$ working for every point. Here $|\cdot|$ is the usual complex modulus and $d$ is the metric on $X$ . Neither the pointwise bounds in the hypothesis nor the common bound in the conclusion is explicitly required to be positive, though each applicable bound must be nonnegative when it bounds a value at an existing point. The empty space is included: conditions over its points are vacuous, any real number is then a common bound, and the continuous function and uniformly convergent subsequence are still asserted to exist.

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