Theorems 7.24-7.25 — Arzelà–Ascoli

Proved

Rudin.ch07_arzela_ascoli

by Lucas · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysistopology

Let $K$ be a compact metric space and $\{f_n\}$ a sequence of continuous complex functions on $K$ which is pointwise bounded and equicontinuous. Then $\{f_n\}$ is uniformly bounded and contains a uniformly convergent subsequence.

Preamble

import Mathlib
import Definitions.Def_Rudin_ch07_families

open Filter Topology

Formal statement

namespace Rudin

/-- Rudin, Theorems 7.24 and 7.25 (Arzelà–Ascoli): a pointwise bounded, equicontinuous sequence
of continuous functions on a compact metric space is uniformly bounded and has a uniformly
convergent subsequence. -/
theorem ch07_arzela_ascoli {K : Type*} [MetricSpace K] [CompactSpace K] (f : ℕ → K → ℂ)
    (hcont : ∀ n, Continuous (f n))
    (hbdd : PointwiseBoundedOn f Set.univ) (heq : EquicontinuousOn f Set.univ) :
    UniformlyBoundedOn f Set.univ ∧
    ∃ φ : ℕ → ℕ, StrictMono φ ∧ ∃ g : K → ℂ,
      TendstoUniformlyOn (fun k => f (φ k)) g atTop Set.univ := by sorry

end Rudin

Source

Walter Rudin, Principles of Mathematical Analysis, 3rd edition, McGraw-Hill, 1976, Chapter 7, pp. 157-158, Theorems 7.24 and 7.25

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

Let $K$ be a metric space that is compact as a whole space, and let $f_0,f_1,\dots : K \to \mathbb{C}$ satisfy:

each $f_n$ is continuous on $K$ ;
pointwise boundedness on all of $K$ : for every $x \in K$ there is a real $M$ (depending on $x$ ) with $\lVert f_n(x)\rVert \le M$ for all $n$ ;
equicontinuity on all of $K$ : for every $\varepsilon>0$ there is $\delta>0$ such that for all $n$ and all $x,y \in K$ with $d(x,y)<\delta$ , $\lVert f_n(x)-f_n(y)\rVert < \varepsilon$ .

Then both:

uniform boundedness: there is a single real $M$ with $\lVert f_n(x)\rVert \le M$ for all $n$ and all $x \in K$ ;
there exist a strictly increasing $\varphi : \mathbb{N}\to\mathbb{N}$ and a function $g : K \to \mathbb{C}$ such that $f_{\varphi(k)} \to g$ uniformly on $K$ as $k \to \infty$ .

Nothing is asserted about continuity of the limit $g$ , and $K$ is allowed to be empty.

Human review

Endorsed by Shuze Chen · Sep 13, 2026
Endorsed by Lucas · Sep 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph