Theorem 7.8 — the uniform Cauchy criterion

Proved

Rudin.ch07_uniform_cauchy

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

analysis

A sequence of complex functions converges uniformly on $E$ if and only if for every $\varepsilon > 0$ there is $N$ such that $|f_n(x) - f_m(x)| \le \varepsilon$ for all $m, n \ge N$ and all $x \in E$ .

Preamble

import Mathlib
import Definitions.Def_Rudin_ch07_families

open Filter Topology

Formal statement

namespace Rudin

/-- Rudin, Theorem 7.8: a sequence of functions converges uniformly on `E` if and only if it
satisfies the uniform Cauchy criterion on `E`. -/
theorem ch07_uniform_cauchy {X : Type*} (E : Set X) (f : ℕ → X → ℂ) :
    (∃ g : X → ℂ, TendstoUniformlyOn f g atTop E) ↔
      ∀ ε : ℝ, 0 < ε → ∃ N : ℕ, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ E, ‖f n x - f m x‖ ≤ ε := by sorry

end Rudin

Source

Walter Rudin, Principles of Mathematical Analysis, 3rd edition, McGraw-Hill, 1976, Chapter 7, p. 147, Theorem 7.8

Read-back

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

Let $X$ be an arbitrary type (no structure), $E \subseteq X$ and $f_0,f_1,\dots$ a sequence of functions $X \to \mathbb{C}$ . The following are equivalent:

there exists $g : X \to \mathbb{C}$ such that $f_n \to g$ uniformly on $E$ ;
for every real $\varepsilon > 0$ there is $N \in \mathbb{N}$ such that for all $m \ge N$ , all $n \ge N$ and all $x \in E$ ,

\lVert f_n(x) - f_m(x) \rVert \le \varepsilon .

The Cauchy estimate is non-strict ( $\le \varepsilon$ ), and the limit function $g$ in the first condition is a function on all of $X$ , unconstrained off $E$ . For $E = \emptyset$ both conditions hold.

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