slope_pos_iff_gt — Mathlib

English

Let 𝕜 be a field with a linear order. For a function f: 𝕜 → 𝕜 and x0 < b, the statement 0 < slope f x0 b is equivalent to f(b) > f(x0).

Русский

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

LaTeX

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

Lean4

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

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