exists_deriv_eq_zero — Mathlib

English

There exists c ∈ (a,b) with deriv f c = 0 under Rolle-type hypotheses with differentiability on the interior.

Русский

Существует c ∈ (a,b) такое, что deriv f c = 0 при аналогичных условия Ролля с производной внутри.

LaTeX

$$$a

Lean4

/-- **Rolle's Theorem** `deriv` version -/ theorem exists_deriv_eq_zero (hab : a < b) (hfc : ContinuousOn f (Icc a b)) (hfI : f a = f b) : ∃ c ∈ Ioo a b, deriv f c = 0 := let ⟨c, cmem, hc⟩ := exists_isLocalExtr_Ioo hab hfc hfI ⟨c, cmem, hc.deriv_eq_zero⟩

Похожие утверждения