slope_pos_iff — Mathlib

English

Let 𝕜 be a field with a linear order. For any f: 𝕜 → 𝕜 and x0 < b, the slope of f from x0 to b is positive if and only if f(x0) < f(b).

Русский

Пусть 𝕜 — поле с линейным порядком. Для любой функции f: 𝕜 → 𝕜 и x0 < b наклон slope f x0 b > 0 тогда выполняется эквивалентно f(x0) < f(b).

LaTeX

$$$\text{If } x_0 < b,\ 0 < \operatorname{slope} f(x_0,b) \iff f(x_0) < f(b).$$$

Lean4

theorem slope_pos_iff {𝕜} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {f : 𝕜 → 𝕜} {x₀ b : 𝕜} (hb : x₀ < b) :
    0 < slope f x₀ b ↔ f x₀ < f b := by simp [slope, hb]

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