lean_workbook_plus_51325

Proved

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

Given the sequence of functions $f_n(x) = \begin{cases} \sqrt{n}, & 0 \leq x \leq \frac{1}{n} \\ 0, & \frac{1}{n} < x \leq 1 \end{cases}$ , where $n \geq 1$ , show that it does not converge uniformly on $[0, 1]$ using the provided counterexample.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_51325 (f : ℕ → ℝ → ℝ) (hf : ∀ n, ∀ x, f n x = if 0 ≤ x ∧ x ≤ 1 / n then Real.sqrt n else 0) : ¬ ∀ ε > 0, ∃ N, ∀ n > N, ∀ x ∈ Set.Icc 0 1, |f n x - 0| < ε   :=  by sorry

Source

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

View graph