English
In a LinearOrder, the comparator cmp a b indeed compares a and b: (cmp a b).Compares a b.
Русский
Для линейного порядка cmp a b действительно сравнивает a и b: (cmp a b).Compares a b.
LaTeX
$$$[LinearOrder \alpha] (a b : \alpha) : (cmp a b).Compares a b$$$
Lean4
theorem cmp_compares [LinearOrder α] (a b : α) : (cmp a b).Compares a b := by
obtain h | h | h := lt_trichotomy a b <;> simp [cmp, cmpUsing, h, h.not_gt]