slope_pos_iff_of_le — Mathlib

English

If x < y and f is strictly increasing, then slope f x y > 0; conversely if f x < f y.

Русский

Если x < y и f строго возрастает, то наклон f x y > 0; наоборот, если f x < f y, то наклон положителен.

LaTeX

$$$x < y \Rightarrow \operatorname{slope}(f,x,y) > 0 \iff f(x) < f(y)$$$

Lean4

theorem slope_pos_iff_of_le (hxy : x ≤ y) : 0 < slope f x y ↔ f x < f y := by
  simp_rw [lt_iff_le_and_ne, slope_nonneg_iff_of_le hxy, Ne, eq_comm, slope_eq_zero_iff]

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