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 : ℝ} :
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.