cmp_eq — Mathlib

English

For any m,n in Num, cmp m n = Ordering.eq if and only if m = n.

Русский

Для любых m,n ∈ Num, cmp m n = Ordering.eq эквивалентно m = n.

LaTeX

$$$cmp\, m\, n = \mathrm{Ordering}.eq \iff m = n$$$

Lean4

theorem cmp_eq (m n) : cmp m n = Ordering.eq ↔ m = n :=
  by
  have := cmp_to_nat m n
  revert this;
  cases cmp m n <;> intro this <;> simp at this ⊢ <;>
      try { exact this
      } <;>
    simp [show m ≠ n from fun e => by rw [e] at this; exact lt_irrefl _ this]

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