compare_iff — Mathlib

English

For any a,b and any o, compare(a,b) = o iff o.Compares(a,b).

Русский

Для любых a,b и любого o верно, что compare(a,b) = o тогда и только тогда, когда o.Compares(a,b).

LaTeX

$$$\operatorname{compare}(a,b) = o \iff o.Compares(a,b)$$$

Lean4

theorem compare_iff (a b : α) {o : Ordering} : compare a b = o ↔ o.Compares a b :=
  by
  cases o <;> simp only [Ordering.Compares]
  · exact compare_lt_iff_lt
  · exact compare_eq_iff_eq
  · exact compare_gt_iff_gt

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