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