exists_hasDerivAt_eq_zero' — Mathlib

English

For a function on an open interval with limits at endpoints, there is a point c ∈ (a,b) with derivative zero provided the endpoint behavior converges to a common limit and differentiability holds on the interior when applicable.

Русский

Для функции на открытом интервале с пределами в концах существует точка c∈(a,b), где производная равна нулю, при условии соответствующего поведения пределов и дифференцируемости внутри.

LaTeX

$$$a

Lean4

/-- **Rolle's Theorem**, a version for a function on an open interval: if `f` has derivative `f'` on `(a, b)` and has the same limit `l` at `𝓝[>] a` and `𝓝[<] b`, then `f' c = 0` for some `c ∈ (a, b)`. -/ theorem exists_hasDerivAt_eq_zero' (hab : a < b) (hfa : Tendsto f (𝓝[>] a) (𝓝 l)) (hfb : Tendsto f (𝓝[<] b) (𝓝 l)) (hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x) : ∃ c ∈ Ioo a b, f' c = 0 := let ⟨c, cmem, hc⟩ := exists_isLocalExtr_Ioo_of_tendsto hab (fun x hx ↦ (hff' x hx).continuousAt.continuousWithinAt) hfa hfb ⟨c, cmem, hc.hasDerivAt_eq_zero <| hff' c cmem⟩

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