Theorem 7.11 — interchanging two limits

Proved

Rudin.ch07_interchange_limits

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

analysis

Suppose $f_n \to g$ uniformly on $E$ , $x$ is a limit point of $E$ , and $\lim_{t \to x} f_n(t) = A_n$ for each $n$ . Then $\{A_n\}$ converges and $\lim_{t \to x} g(t) = \lim_n A_n$ ; in other words the two limit operations commute.

Preamble

import Mathlib
import Definitions.Def_Rudin_ch07_families

open Filter Topology

Formal statement

namespace Rudin

/-- Rudin, Theorem 7.11: if `f n → g` uniformly on `E`, `x` is a limit point of `E`, and
`f n t → A n` as `t → x` within `E`, then `A n` converges and `g t → lim A n` as `t → x`;
that is, the two limit operations may be interchanged. -/
theorem ch07_interchange_limits {X : Type*} [MetricSpace X] (E : Set X) (f : ℕ → X → ℂ)
    (g : X → ℂ) (A : ℕ → ℂ) (x : X) (hx : x ∈ closure (E \ {x}))
    (huc : TendstoUniformlyOn f g atTop E)
    (hA : ∀ n, Tendsto (f n) (𝓝[E \ {x}] x) (𝓝 (A n))) :
    ∃ L : ℂ, Tendsto A atTop (𝓝 L) ∧ Tendsto g (𝓝[E \ {x}] x) (𝓝 L) := by sorry

end Rudin

Source

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

Read-back

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

Let $X$ be a metric space, $E \subseteq X$ , let $f_0,f_1,\dots : X \to \mathbb{C}$ , $g : X \to \mathbb{C}$ , $A : \mathbb{N} \to \mathbb{C}$ and $x \in X$ . Assume:

$x$ lies in the closure of $E \setminus \{x\}$ (equivalently, $x$ is a limit point of $E$ );
$f_n \to g$ uniformly on $E$ ;
for every $n$ , $f_n(t) \to A_n$ as $t \to x$ through the points of $E$ other than $x$ .

Then there exists $L \in \mathbb{C}$ such that both

A_n \xrightarrow[n\to\infty]{} L \qquad\text{and}\qquad g(t) \xrightarrow[t \to x,\ t \in E\setminus\{x\}]{} L .

So the sequence of limit values converges and the limit function has the same limit at $x$ along the punctured set. The value $g(x)$ itself plays no role.

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