lt_to_int — Mathlib

English

For all m,n ∈ ZNum, (m : ℤ) < n iff m < n.

Русский

Для всех m,n ∈ ZNum, (m : ℤ) < n тогда и только тогда, когда m < n.

LaTeX

$$$$\forall m,n \in ZNum,\ ( (m : \mathbb{Z}) < n ) \leftrightarrow m < n.$$$$

Lean4

@[norm_cast]
theorem lt_to_int {m n : ZNum} : (m : ℤ) < n ↔ m < n :=
  show (m : ℤ) < n ↔ cmp m n = Ordering.lt from
    match cmp m n, cmp_to_int m n with
    | Ordering.lt, h => by simp only at h; simp [h]
    | Ordering.eq, h => by simp only at h; simp [h]
    | Ordering.gt, h => by simp [not_lt_of_gt h]

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