slope_nonpos_iff_of_le — Mathlib

English

If f is a function into an ordered abelian group (or ordered space), slope nonnegativity corresponds to f being nondecreasing.

Русский

Если функция t направлена в упорядоченную группу, неотрицательность наклона эквивалентна неубываемости функции.

LaTeX

$$$0 \le \operatorname{slope} f x y \iff f(x) \le f(y)$ (при x ≤ y)$$

Lean4

theorem slope_nonpos_iff_of_le (hxy : x ≤ y) : slope f x y ≤ 0 ↔ f y ≤ f x := by
  simpa using slope_nonneg_iff_of_le (f := -f) hxy

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