lean_workbook_plus_71388

Proved

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

Since $-1\leq f(x)\leq 1$ , then $f(x+am)-f(x)$ is bounded.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_71388 (f : ℝ → ℝ) (m : ℝ) (hf: ∀ x, -1 ≤ f x ∧ f x ≤ 1) : ∃ M, ∀ x, |f (x + m) - f x| ≤ M   :=  by sorry

Source