lt_to_nat — Mathlib

English

For all m,n in PosNum, (m : ℕ) < n ↔ m < n.

Русский

Для любых m,n из PosNum, (m : ℕ) < n эквивалентно m < n.

LaTeX

$$$(m : \\mathbb{N}) < n \\iff m < n$$$

Lean4

@[norm_cast]
theorem lt_to_nat {m n : PosNum} : (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]

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