# 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 exists_hasDerivWithinAt_eq_of_gt_of_lt {a : } {b : } {f : } {f' : } (hab : a b) (hf : xSet.Icc a b, HasDerivWithinAt f (f' x) (Set.Icc a b) x) {m : } (hma : f' a < m) (hmb : m < f' b) :
m f' '' Set.Ioo a b

Darboux's theorem: if a ≤ b and f' a < m < f' b, then f' c = m for some c ∈ (a, b).

theorem exists_hasDerivWithinAt_eq_of_lt_of_gt {a : } {b : } {f : } {f' : } (hab : a b) (hf : xSet.Icc a b, HasDerivWithinAt f (f' x) (Set.Icc a b) x) {m : } (hma : m < f' a) (hmb : f' b < m) :
m f' '' Set.Ioo a b

Darboux's theorem: if a ≤ b and f' b < m < f' a, then f' c = m for some c ∈ (a, b).

theorem Set.OrdConnected.image_hasDerivWithinAt {f : } {f' : } {s : } (hs : s.OrdConnected) (hf : xs, HasDerivWithinAt f (f' x) s x) :
(f' '' s).OrdConnected

Darboux's theorem: the image of a Set.OrdConnected set under f' is a Set.OrdConnected set, HasDerivWithinAt version.

theorem Set.OrdConnected.image_derivWithin {f : } {s : } (hs : s.OrdConnected) (hf : ) :
( '' s).OrdConnected

Darboux's theorem: the image of a Set.OrdConnected set under f' is a Set.OrdConnected set, derivWithin version.

theorem Set.OrdConnected.image_deriv {f : } {s : } (hs : s.OrdConnected) (hf : xs, ) :
( '' s).OrdConnected

Darboux's theorem: the image of a Set.OrdConnected set under f' is a Set.OrdConnected set, deriv version.

theorem Convex.image_hasDerivWithinAt {f : } {f' : } {s : } (hs : ) (hf : xs, HasDerivWithinAt f (f' x) s x) :
Convex (f' '' s)

Darboux's theorem: the image of a convex set under f' is a convex set, HasDerivWithinAt version.

theorem Convex.image_derivWithin {f : } {s : } (hs : ) (hf : ) :

Darboux's theorem: the image of a convex set under f' is a convex set, derivWithin version.

theorem Convex.image_deriv {f : } {s : } (hs : ) (hf : xs, ) :

Darboux's theorem: the image of a convex set under f' is a convex set, deriv version.

theorem exists_hasDerivWithinAt_eq_of_ge_of_le {a : } {b : } {f : } {f' : } (hab : a b) (hf : xSet.Icc a b, HasDerivWithinAt f (f' x) (Set.Icc a b) x) {m : } (hma : f' a m) (hmb : m f' b) :
m f' '' Set.Icc a b

Darboux's theorem: if a ≤ b and f' a ≤ m ≤ f' b, then f' c = m for some c ∈ [a, b].

theorem exists_hasDerivWithinAt_eq_of_le_of_ge {a : } {b : } {f : } {f' : } (hab : a b) (hf : xSet.Icc a b, HasDerivWithinAt f (f' x) (Set.Icc a b) x) {m : } (hma : f' a m) (hmb : m f' b) :
m f' '' Set.Icc a b

Darboux's theorem: if a ≤ b and f' b ≤ m ≤ f' a, then f' c = m for some c ∈ [a, b].

theorem hasDerivWithinAt_forall_lt_or_forall_gt_of_forall_ne {f : } {f' : } {s : } (hs : ) (hf : xs, HasDerivWithinAt f (f' x) s x) {m : } (hf' : xs, f' x m) :
(∀ xs, f' x < m) xs, m < f' x

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.