Derivative_of_Monotone_Function

Proved

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

calculusderivativesmonotone-functionsproofwiki

If f is continuous on [a,b], differentiable on (a,b), and monotone increasing, then f'(x) >= 0 on (a,b).

Preamble

import Mathlib.Analysis.Complex.Basic
import Mathlib.Analysis.Calculus.MeanValue

Formal statement

import Mathlib.Analysis.Complex.Basic
import Mathlib.Analysis.Calculus.MeanValue

theorem Derivative_of_Monotone_Function (f : ℝ → ℝ) (a b : ℝ) (hab : a < b) (hfc : ContinuousOn f (Set.Icc a b)) (hfd : DifferentiableOn ℝ f (Set.Ioo a b)) (hf_mono : MonotoneOn f (Set.Icc a b)) : ∀ x ∈ Set.Ioo a b, 0 ≤ deriv f x := by sorry

Source

https://proofwiki.org/wiki/Derivative_of_Monotone_Function

View graph