lean_workbook_plus_12581

Proved

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

Prove that if a sequence $x_n$ converges to $x$ and $f$ is a continuous function, then $f(x_n)$ converges to $f(x)$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_12581 (x : ℕ → ℝ) (f : ℝ → ℝ) (hf: Continuous f) (hx: ∃ a, ∀ ε, 0 < ε → ∃ N, ∀ n, N ≤ n → |x n - a| < ε) : ∃ a, ∀ ε, 0 < ε → ∃ N, ∀ n, N ≤ n → |f (x n) - a| < ε   :=  by sorry

Source

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

View graph