Absolutely_Continuous_Real_Function_is_Continuous

Proved

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

absolutely-continuous-functionscontinuous-real-functionsproofwiki

Let $I \subseteq \R$ be a real interval. Let $f : I \to \R$ be an absolutely continuous function. Then $f$ is continuous.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Absolutely_Continuous_Real_Function_is_Continuous (f : ℝ → ℝ) (hf : ∀ ε > 0, ∃ δ > 0, ∀ a b : ℝ, |b - a| < δ → |f b - f a| < ε) : Continuous f := by sorry

Source

https://proofwiki.org/wiki/Absolutely_Continuous_Real_Function_is_Continuous

View graph