le_iff_cmp — Mathlib

English

In Num, m ≤ n iff m.cmp n ≠ Ordering.gt; equivalently, m ≤ n iff not (m > n).

Русский

В Num, m ≤ n эквивалентно m.cmp n ≠ Ordering.gt; иначе говоря, m ≤ n, если не выполняется m > n.

LaTeX

$$$\\forall {m\\, n : \\text{Num}}, \\; \\operatorname{LE}.le\, m\\, n \iff (m.{\\mathrm{cmp}}\\, n) \\neq \\mathrm{Ordering}.gt$$$

Lean4

theorem le_iff_cmp {m n} : m ≤ n ↔ cmp m n ≠ Ordering.gt :=
  not_congr <| lt_iff_cmp.trans <| by rw [← cmp_swap]; cases cmp m n <;> decide

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