English
In a linear order, the comparison function is a lawful boolean comparator with the specified properties.
Русский
В линейном порядке функция сравнения является законной булевой компараторой с заданными свойствами.
LaTeX
$$$\mathrm{Std.LawfulBCmp}(\mathrm{compare})$$$
Lean4
instance : Std.LawfulBCmp (compare (α := α))
where
eq_swap
{a
b} := by
cases _ : compare b a <;> simp_all [Ordering.swap, compare_eq_iff_eq, compare_lt_iff_lt, compare_gt_iff_gt]
isLE_trans h₁
h₂ := by
simp only [← Ordering.ne_gt_iff_isLE, compare_le_iff_le] at *
exact le_trans h₁ h₂
compare_eq_iff_beq := by simp [compare_eq_iff_eq]
eq_lt_iff_lt := by simp [compare_lt_iff_lt]
isLE_iff_le := by simp [← Ordering.ne_gt_iff_isLE, compare_le_iff_le]