exists_deriv_eq_zero' — Mathlib

English

If hab < b, hfc ensures continuity on [a,b] and f(a)=f(b), then ∃ c ∈ (a,b) with deriv f c = 0.

Русский

Если a<b, функция непрерывна на [a,b] и f(a)=f(b), то существует c∈(a,b), такой что производная в c равна нулю.

LaTeX

$$$a

Lean4

/-- **Rolle's Theorem**, a version for a function on an open interval: if `f` has the same limit `l` at `𝓝[>] a` and `𝓝[<] b`, then `deriv f c = 0` for some `c ∈ (a, b)`. This version does not require differentiability of `f` because we define `deriv f c = 0` whenever `f` is not differentiable at `c`. -/ theorem exists_deriv_eq_zero' (hab : a < b) (hfa : Tendsto f (𝓝[>] a) (𝓝 l)) (hfb : Tendsto f (𝓝[<] b) (𝓝 l)) : ∃ c ∈ Ioo a b, deriv f c = 0 := by by_cases h : ∀ x ∈ Ioo a b, DifferentiableAt ℝ f x · exact exists_hasDerivAt_eq_zero' hab hfa hfb fun x hx => (h x hx).hasDerivAt · obtain ⟨c, hc, hcdiff⟩ : ∃ x ∈ Ioo a b, ¬DifferentiableAt ℝ f x := by push_neg at h; exact h exact ⟨c, hc, deriv_zero_of_not_differentiableAt hcdiff⟩

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