deriv_neg_right_of_sign_deriv — Mathlib

English

If a left-right pattern holds for the sign of the derivative, then the derivatives to the right of the point are negative in a neighborhood.

Русский

Если выполняется заданный знак производной справа от точки, то справа от точки производные отрицательны в окрестности.

LaTeX

$$$$\\forall b\\text{ near } x_0\\ (b>x_0)\\ \\Rightarrow \\ deriv f(b)<0 \\text{ under the sign condition}. $$$$

Lean4

theorem deriv_neg_right_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 [nhdsGT_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

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