Theorem 7.12 — uniform limits of continuous functions

Proved

Rudin.ch07_uniform_limit_continuous

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

analysistopology

If each $f_n$ is continuous on $E$ and $f_n \to g$ uniformly on $E$ , then $g$ is continuous on $E$ .

Preamble

import Mathlib
import Definitions.Def_Rudin_ch07_families

open Filter Topology

Formal statement

namespace Rudin

/-- Rudin, Theorem 7.12: a uniform limit of continuous functions is continuous. -/
theorem ch07_uniform_limit_continuous {X : Type*} [MetricSpace X] (E : Set X) (f : ℕ → X → ℂ)
    (g : X → ℂ) (hcont : ∀ n, ContinuousOn (f n) E) (huc : TendstoUniformlyOn f g atTop E) :
    ContinuousOn g E := by sorry

end Rudin

Source

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

Read-back

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

Let $X$ be a metric space, $E \subseteq X$ , and let $f_0,f_1,\dots : X \to \mathbb{C}$ and $g : X \to \mathbb{C}$ . If every $f_n$ is continuous on $E$ (relative continuity at each point of $E$ ) and $f_n \to g$ uniformly on $E$ , then $g$ is continuous on $E$ .

Continuity is relative to $E$ throughout, so nothing is assumed or concluded about behaviour at points outside $E$ ; and $E$ may be empty, in which case the conclusion is trivial.

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