eventually_nhdsWithin_sign_eq_of_deriv_neg

English

If at a root x0 the derivative is negative, then near x0 the sign of f(x) matches the sign of x0−x.

Русский

Если в корне x0 производная отрицательна, то знак f(x) близко к x0 совпадает с знаком x0−x.

LaTeX

$$$$\\text{If } f(x_0)=0,\\ f'(x_0)<0,\\text{ then } \\operatorname{sign}(f(x))=\\operatorname{sign}(x_0-x)\\text{ near } x_0.$$$$

Lean4

/-- If the derivative of `f` is negative at a root `x₀` of `f`, then locally the sign of `f x`
matches `x₀ - x`. -/
theorem eventually_nhdsWithin_sign_eq_of_deriv_neg (hf : deriv f x₀ < 0) (hx : f x₀ = 0) :
    ∀ᶠ x in 𝓝 x₀, sign (f x) = sign (x₀ - x) := by
  simpa [Left.sign_neg, -neg_sub, ← neg_sub x₀] using
    eventually_nhdsWithin_sign_eq_of_deriv_pos (f := (-f ·)) (x₀ := x₀) (by simpa [deriv.neg]) (by simpa)

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