English
If α and β are LinearOrder, then Lex(α × β) is a LinearOrder.
Русский
Если α и β — линейно упорядоченные, то Lex(α × β) — линейно упорядочено.
LaTeX
$$$$ (\alpha \times_\mathrm{lex} \beta) \text{ is a LinearOrder whenever } \alpha, \beta \text{ are LinearOrder}. $$$$
Lean4
/-- Dictionary / lexicographic linear order for pairs. -/
instance instLinearOrder (α β : Type*) [LinearOrder α] [LinearOrder β] : LinearOrder (α ×ₗ β) :=
{ Prod.Lex.instPartialOrder α β with
le_total := total_of (Prod.Lex _ _)
toDecidableLE := Prod.Lex.decidable _ _
toDecidableLT := Prod.Lex.decidable _ _
toDecidableEq := instDecidableEqLex _
compare_eq_compareOfLessAndEq := fun a b =>
by
have : DecidableLT (α ×ₗ β) := Prod.Lex.decidable _ _
have : Std.LawfulBEqOrd (α ×ₗ β) := ⟨by simp [compare_def, compareLex, compareOn, Ordering.then_eq_eq]⟩
have : Std.LawfulLTOrd (α ×ₗ β) :=
⟨by simp [compare_def, compareLex, compareOn, Ordering.then_eq_lt, toLex_lt_toLex, compare_lt_iff_lt]⟩
convert Std.LawfulLTCmp.eq_compareOfLessAndEq (cmp := compare) a b }
