English
Let a ≤ b. If for every x in [a,b] the derivative f′(x) is realized by HasDerivWithinAt f (f′(x)) on [a,b], and if f′(a) ≤ m ≤ f′(b), then m occurs as a derivative value inside [a,b]; i.e., m ∈ f′[a,b].
Русский
Пусть a ≤ b. Если для каждого x в [a,b] существует такая производная f′(x), что f имеет внутри [a,b] производную f′(x) в точке x, и f′(a) ≤ m ≤ f′(b), тогда существует c ∈ [a,b], для которого f′(c) = m.
LaTeX
$$$a \le b \land \forall x \in Icc(a,b), HasDerivWithinAt f (f'(x)) (Icc a b) x \land f'(a) \le m \le f'(b) \Rightarrow m \in f' '' Icc(a,b)$$$
Lean4
/-- **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_ge_of_le (hab : a ≤ b) (hf : ∀ x ∈ Icc a b, HasDerivWithinAt f (f' x) (Icc a b) x)
{m : ℝ} (hma : f' a ≤ m) (hmb : m ≤ f' b) : m ∈ f' '' Icc a b :=
(ordConnected_Icc.image_hasDerivWithinAt hf).out (mem_image_of_mem _ (left_mem_Icc.2 hab))
(mem_image_of_mem _ (right_mem_Icc.2 hab)) ⟨hma, hmb⟩
