strictAntiOn_natAbs — Mathlib

English

The absolute value function is strictly decreasing on the nonpositive integers: if a ≤ b ≤ 0 and a < b then |a| > |b|.

Русский

Функция модуля строго возвращает убывание на неотрицательных целых числах: если a ≤ b ≤ 0 и a < b, то |a| > |b|.

LaTeX

$$$\forall a,b \in \mathbb{Z},\ a \le 0,\ b \le 0,\ a < b \Rightarrow |a| > |b|$$$

Lean4

theorem strictAntiOn_natAbs : StrictAntiOn natAbs (Iic 0) := fun a _ b hb hab => by
  simpa [Int.natAbs_neg] using natAbs_lt_natAbs_of_nonneg_of_lt (Right.nonneg_neg_iff.mpr hb) (neg_lt_neg_iff.mpr hab)

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