Proposition 11.6.5 — Pointwise subsequence on a countable set

Proved

LeblRA.pointwise_subsequence_11_6_5

by wamlart · Sep 6, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

analysisarzela-ascolicompactnessuniform-convergence

Let $X$ be any countable set and let $F_n:X\to\mathbb C$ be a sequence of functions. Assume pointwise boundedness:

\forall x\in X\;\exists M_x\in\mathbb R\;\forall n\in\mathbb N,\qquad |F_n(x)|\le M_x.

Then there exist a strictly increasing map $\varphi:\mathbb N\to\mathbb N$ and a function $f:X\to\mathbb C$ such that

\forall x\in X,\qquad F_{\varphi(n)}(x)\longrightarrow f(x)\quad(n\to\infty).

This is the countable-domain subsequence result in Lebl’s Proposition 11.6.5.

Formalization Note. $X$ carries no topology, and no continuity assumption is made. Finite and empty sets are included. The formal sequence starts at zero rather than one; this is only a reindexing. Strict increase is represented by StrictMono, and the pointwise limit is explicit.

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 pointwise_subsequence_11_6_5 {X : Type u} [Countable X]
    (F : ℕ → X → ℂ) (hF : ∀ x, ∃ M : ℝ, ∀ n, ‖F n x‖ ≤ M) :
    ∃ (φ : ℕ → ℕ) (f : X → ℂ), StrictMono φ ∧
      ∀ x, Tendsto (fun n => F (φ n) x) atTop (𝓝 (f x)) := by sorry
end LeblRA

Source

Jiří Lebl, Basic Analysis II: Introduction to Real Analysis, Volume II, §11.6, Proposition 11.6.5, 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 at most countable type $X$ , of any universe and with no topology assumed, and every sequence of functions $F_n:X\to\mathbb C$ indexed by all natural numbers $n$ including $0$ , assume that for every $x\in X$ there exists a real number $M$ such that $|F_n(x)|\le M$ for every natural number $n$ . The bound $M$ may depend on $x$ and is not required explicitly to be positive. Then there exist a function $\varphi:\mathbb N\to\mathbb N$ and a function $f:X\to\mathbb C$ such that $\varphi$ is strictly increasing, meaning $\varphi(i)<\varphi(j)$ whenever $i<j$ , and for every $x\in X$ the complex sequence $F_{\varphi(n)}(x)$ converges to $f(x)$ as $n\to\infty$ . Explicitly, for each $x\in X$ and each real $\varepsilon>0$ , there is a natural number $N$ , which may depend on $x$ and $\varepsilon$ , such that $|F_{\varphi(n)}(x)-f(x)|<\varepsilon$ for every $n\ge N$ . The same $\varphi$ works for every $x$ , and its value at $0$ is not prescribed. Here $|\cdot|$ is the usual complex modulus. Finite and empty $X$ are included; when $X$ is empty, the boundedness and convergence conditions over $x$ are vacuous. At any point that exists, the bound in the hypothesis must be nonnegative because it bounds a modulus for $n=0$ .

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