Darboux's theorem #
In this file we prove that the derivative of a differentiable function on an interval takes all intermediate values. The proof is based on the Wikipedia page about this theorem.
theorem
deriv_forall_lt_or_forall_gt_of_forall_ne
{f f' : ℝ → ℝ}
{s : set ℝ}
(hs : convex ℝ s)
(hf : ∀ (x : ℝ), x ∈ s → has_deriv_at f (f' x) x)
{m : ℝ}
(hf' : ∀ (x : ℝ), x ∈ s → f' x ≠ m) :
If the derivative of a function is never equal to m
, then either
it is always greater than m
, or it is always less than m
.