compare_def — Mathlib

English

The compare operation on α ×ₗ β equals the lexicographic compare of the first and second coordinates.

Русский

Операция сравнения на α ×ₗ β равна лексикографическому сравнению первая/вторая координат.

LaTeX

$$$$ \text{compare}(\alpha \times_\mathrm{lex} \beta) = \mathrm{compareLex}(\mathrm{compareOn}(\cdot_1), \mathrm{compareOn}(\cdot_2)). $$$$

Lean4

theorem compare_def [Ord α] [Ord β] :
    @compare (α ×ₗ β) _ = compareLex (compareOn fun x => (ofLex x).1) (compareOn fun x => (ofLex x).2) :=
  rfl

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