lean_workbook_plus_9130

Proved

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

Since $f$ is uniformly continuous on $[x,x+1]$ , for any $\epsilon > 0$ we can find a $\delta > 0$ such that $|t_1 - t_2| < \delta \implies |f(t_1) - f(t_2)| < \epsilon$ holds for $t_1,t_2 \in [x,x+1]$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_9130 {f : ℝ → ℝ} {x : ℝ} :
  UniformContinuousOn f (Set.Icc x (x + 1)) ↔
    ∀ ε > 0, ∃ δ > 0, ∀ t1 t2 : ℝ, t1 ∈ Set.Icc x (x + 1) ∧ t2 ∈ Set.Icc x (x + 1) ∧
      |t1 - t2| < δ → |f t1 - f t2| < ε   :=  by sorry

Source

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

View graph