exists_hasDerivAt_eq_zero — Mathlib

English

Let f be a function on an interval with f continuous on [a,b], f(a) = f(b). If f is differentiable on (a,b), then there exists c ∈ (a,b) with f'(c) = 0.

Русский

Пусть функция f определена на интервале; если f непрерывна на [a,b], f(a)=f(b) и дифференцируема на (a,b), то существует c в (a,b) такое, что f'(c)=0.

LaTeX

$$$a

Lean4

/-- **Rolle's Theorem** `HasDerivAt` version -/ theorem exists_hasDerivAt_eq_zero (hab : a < b) (hfc : ContinuousOn f (Icc a b)) (hfI : f a = f b) (hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x) : ∃ c ∈ Ioo a b, f' c = 0 := let ⟨c, cmem, hc⟩ := exists_isLocalExtr_Ioo hab hfc hfI ⟨c, cmem, hc.hasDerivAt_eq_zero <| hff' c cmem⟩

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