slope_neg_iff_of_le — Mathlib

English

Let f: k → E be a function into an ordered additive group E, and let x ≤ y be elements of k. Then the slope of f between x and y is negative if and only if f(y) < f(x) (provided we compare with respect to the natural order on E).

Русский

Пусть f: k → E, где E — упорядоченная аддитивная группа, и пусть x ≤ y. Тогда уклон ориентированной секции slope f x y отрицателен тогда и только тогда, когда f(y) < f(x).

LaTeX

$$$x \\le y \\implies \\left( \\operatorname{slope} f x y < 0 \\iff f(y) < f(x) \\right)$$$

Lean4

theorem slope_neg_iff_of_le (hxy : x ≤ y) : slope f x y < 0 ↔ f y < f x := by
  simpa using slope_pos_iff_of_le (f := -f) hxy

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