neg_of_slope_pos — Mathlib

English

If x0 > b and the slope from x0 to b is positive, with f(x0) = 0, then f(b) < 0.

Русский

Если x0 > b, наклон slope f(x0,b) > 0, и f(x0) = 0, то f(b) < 0.

LaTeX

$$$x_0 > b \land 0 < \operatorname{slope} f(x_0,b) \land f(x_0)=0 \Longrightarrow f(b) < 0.$$$

Lean4

theorem neg_of_slope_pos {𝕜} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {f : 𝕜 → 𝕜} {x₀ b : 𝕜} (hb : b < x₀)
    (hbf : 0 < slope f x₀ b) (hf : f x₀ = 0) : f b < 0 :=
  by
  rwa [slope_pos_iff_gt, hf] at hbf
  exact hb

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