lt_to_nat — Mathlib

English

For all m,n, the natural-number less-than comparison agrees with the Num order: (m:ℕ) < n iff m < n.

Русский

Для любых m,n: сравнение меньше-числа по натуральным чисам совпадает с порядком Num: (m:ℕ) < n ⇔ m < n.

LaTeX

$$$\\forall {m,n : Num}, (m : \\mathbb{N}) < n \\Leftrightarrow m < n$$$

Lean4

@[norm_cast]
theorem lt_to_nat {m n : Num} : (m : ℕ) < n ↔ m < n :=
  show (m : ℕ) < n ↔ cmp m n = Ordering.lt from
    match cmp m n, cmp_to_nat m n with
    | Ordering.lt, h => by simp [h]
    | Ordering.eq, h => by simp [h]
    | Ordering.gt, h => by simp [not_lt_of_gt h]

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