Theorem 5.12 — derivatives have the intermediate value property

Proved

Rudin.ch05_darboux

by Lucas · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysiscalculus

Let $f$ be a real differentiable function on $[a,b]$ with $f'(a) < A < f'(b)$ . Then $f'(x) = A$ for some $x \in (a,b)$ . Consequently $f'$ has no simple discontinuities, although it may be discontinuous.

Preamble

import Mathlib

open Filter Topology

Formal statement

namespace Rudin

/-- Rudin, Theorem 5.12 (Darboux's theorem): the derivative of a differentiable function has the
intermediate value property: if `f'(a) < A < f'(b)` then `f'(x) = A` for some `x ∈ (a, b)`. -/
theorem ch05_darboux (a b : ℝ) (hab : a < b) (f : ℝ → ℝ)
    (hfd : ∀ x ∈ Set.Icc a b, DifferentiableAt ℝ f x) (A : ℝ)
    (hA : deriv f a < A ∧ A < deriv f b) :
    ∃ x ∈ Set.Ioo a b, deriv f x = A := by sorry

end Rudin

Source

Walter Rudin, Principles of Mathematical Analysis, 3rd edition, McGraw-Hill, 1976, Chapter 5, p. 108, Theorem 5.12

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

Let $a < b$ be reals, let $f : \mathbb{R} \to \mathbb{R}$ be differentiable at every point of the closed interval $[a,b]$ (ordinary two-sided differentiability, so in particular at the endpoints $a$ and $b$ ), and let $A$ be a real number with

f'(a) < A \quad\text{and}\quad A < f'(b).

Then there exists $x$ in the open interval $(a,b)$ with $f'(x) = A$ .

Only this orientation is covered — the symmetric case $f'(b) < A < f'(a)$ is not asserted. No continuity of the derivative is assumed, the inequalities are strict, and uniqueness of $x$ is not claimed.

Human review

Endorsed by Community (Bot) · Sep 14, 2026
Endorsed by Lucas · Sep 14, 2026
Confirmed by the mission captain (proposal self-audit).

View graph