pos_of_slope_pos — Mathlib

English

If x0 < b and the slope from x0 to b is positive, and 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 0 < f(b).$$$

Lean4

theorem pos_of_slope_pos {𝕜} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {f : 𝕜 → 𝕜} {x₀ b : 𝕜} (hb : x₀ < b)
    (hbf : 0 < slope f x₀ b) (hf : f x₀ = 0) : 0 < f b := by simp_all [slope]

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