Proposition 11.6.7 — Uniform convergence implies uniform equicontinuity

Proved

LeblRA.uniform_limit_equicontinuous_11_6_7

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 converging uniformly to $f:X\to\mathbb C$ . Then the sequence is uniformly equicontinuous:

\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.

Thus uniform convergence imposes one continuity condition shared by the entire sequence. This is Lebl’s Proposition 11.6.7.

Formalization Note. The full condition is written out: $\delta$ is independent of $n$ , $x$ , and $y$ . Uniform convergence is TendstoUniformly. No boundedness or nonemptiness assumption is added.

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 uniform_limit_equicontinuous_11_6_7 {X : Type u} [MetricSpace X] [CompactSpace X]
    (F : ℕ → X → ℂ) (hF : ∀ n, Continuous (F n)) (f : X → ℂ)
    (hf : TendstoUniformly F f atTop) :
    ∀ ε > 0, ∃ δ > 0, ∀ x y, dist x y < δ → ∀ n, ‖F n x - F n y‖ < ε := by sorry
end LeblRA

Source

Jiří Lebl, Basic Analysis II: Introduction to Real Analysis, Volume II, §11.6, Proposition 11.6.7, 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 no restriction on its underlying type's universe), every sequence $F_n:X\to\mathbb C$ , indexed by all natural numbers $n$ including $0$ , for which each $F_n$ is continuous, and every function $f:X\to\mathbb C$ , assume that $F_n$ converges uniformly to $f$ : for every real $\eta>0$ there is a natural number $N$ such that $|F_n(x)-f(x)|<\eta$ for every $n\ge N$ and every $x\in X$ . Then, for every real $\varepsilon>0$ , there is a real $\delta>0$ such that, for every $x,y\in X$ with $d(x,y)<\delta$ and every natural number $n$ , one has $|F_n(x)-F_n(y)|<\varepsilon$ . Thus this one $\delta$ works simultaneously for every pair of points and every term of the sequence. Here $|\cdot|$ is the usual complex modulus and $d$ is the metric on $X$ . The empty space is permitted; in that case the conditions and conclusions quantified over points are vacuous. No continuity hypothesis is imposed separately on $f$ .

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