lean_workbook_plus_9417

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

For pointwise convergence, does $f_n(x)$ converge to a limit function $f(x)$ for every $x \in \mathbb{R}$ ?

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_9417 (f : ℕ → ℝ → ℝ) (f_lim : ℝ → ℝ) (hf : ∀ x, ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |f n x - f_lim x| < ε) : ∀ x, ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |f n x - f_lim x| < ε   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph