Prove2Me

lean_workbook_plus_44988

Proved

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

Suppose lim⁡x→0f(x)=0\lim_{x\to0}f(x)=0. Prove that 1) lim⁡x→0(f(x)+f(2x))=0\lim_{x\to0}(f(x)+f(2x))=0, 2) lim⁡x→0(f(x)+f(x2))=0\lim_{x\to0}(f(x)+f(x^2))=0.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_44988 (f : ℝ → ℝ) (h : ∀ ε > 0, ∃ δ > 0, ∀ x, |x| < δ → |f x| < ε) : ∀ ε > 0, ∃ δ > 0, ∀ x, |x| < δ → |f x + f (2 * x)| < ε   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph