English
Let a ≤ b. If f′(b) ≤ m ≤ f′(a) for some m, and HasDerivWithinAt f (f′(x)) (Icc a b) x holds for all x ∈ Icc a b, then m is attained by f′ on [a,b], i.e., m ∈ f′([a,b]).
Русский
Пусть a ≤ b. Если f′(b) ≤ m ≤ f′(a) и для всех x ∈ [a,b] существует такая производная f′(x), что HasDerivWithinAt f (f′(x)) (Icc a b) x, то существует 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 \Rightarrow f'(b) \le m \le f'(a) \Rightarrow m \in f' '' Icc(a,b)$$$
Lean4
/-- **Darboux's theorem**: if `a ≤ b` and `f' b ≤ m ≤ f' a`, then `f' c = m` for some
`c ∈ [a, b]`. -/
theorem exists_hasDerivWithinAt_eq_of_le_of_ge (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⟩
