lean_workbook_plus_20489

Proved

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

Given the definition of limit: $\lim_{x\rightarrow a} f(x)=F$ if for every positive $\epsilon$ , there exists a positive $\delta$ such that if $x\neq a$ and $|x-a|<\delta$ , then $|f(x)-F|<\epsilon$ . Prove that $\lim_{x \to a} f(x) + g(x) = F + G$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_20489 (f g : ℝ → ℝ) (a F G : ℝ) (hf : ∀ ε > 0, ∃ δ > 0, ∀ x, x ≠ a ∧ |x - a| < δ → |f x - F| < ε) (hg : ∀ ε > 0, ∃ δ > 0, ∀ x, x ≠ a ∧ |x - a| < δ → |g x - G| < ε) : ∀ ε > 0, ∃ δ > 0, ∀ x, x ≠ a ∧ |x - a| < δ → |f x + g x - (F + G)| < ε   :=  by sorry

Source

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

View graph