deriv_neg_left_of_sign_deriv — Mathlib

English

If a sign pattern of the derivative holds near a point from the left, then the left-approaching derivatives are negative.

Русский

Если вблизи точки слева знак производной имеет заданный характер, то приближающиеся слева производные отрицательны.

LaTeX

$$$$\\forall b\\text{ near } x_0\\ (b

Lean4

theorem deriv_neg_left_of_sign_deriv {f : ℝ → ℝ} {x₀ : ℝ}
    (h₀ : ∀ᶠ (x : ℝ) in 𝓝[≠] x₀, sign (deriv f x) = sign (x - x₀)) : ∀ᶠ (b : ℝ) in 𝓝[<] x₀, deriv f b < 0 :=
  by
  filter_upwards [nhdsLT_le_nhdsNE _ h₀, self_mem_nhdsWithin] with x hx' (hx : x < x₀)
  rwa [← sub_neg, ← sign_eq_neg_one_iff, ← hx', sign_eq_neg_one_iff] at hx

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