lean_workbook_plus_34658

Proved

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

Let $f$ be an arbitrary continuous function on $[a,b]$ and $\epsilon$ a positive number. Show that there is a polygonal function $\psi$ on $[a,b]$ with $|f(x)-\psi(x)|<\epsilon$ for all $x\in [a,b]$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_34658 (f : ℝ → ℝ) (a b : ℝ) (ε : ℝ) (hf : ContinuousOn f (Set.Icc a b)) (hε : 0 < ε) : ∃ ψ : ℝ → ℝ, ContinuousOn ψ (Set.Icc a b) ∧ ∀ x ∈ Set.Icc a b, |f x - ψ x| < ε   :=  by sorry

Source

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

View graph