instLawfulBCmpCompare_mathlib — Mathlib

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]

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