English
The colexicographic order on the family of all functions f: ι → β_i is a linear order, provided that ι is a linear order with WellFoundedGT and every β_i is a linear order.
Русский
Коэкс-порядок на множестве функций f: ι → β_i образует линейный порядок, если ι — линейный порядок с WellFoundedGT, и для каждого i множество β_i упорядочено линейно.
LaTeX
$$$[ \\text{LinearOrder } \\iota] \\land [ \\text{WellFoundedGT } \\iota] \\land [ \\forall i, \\text{ LinearOrder } (\\beta i)] \\Rightarrow \\text{ LinearOrder }(\\mathrm{Colex}( (i : \\iota) \\to \\beta i)).$$$
Lean4
/-- `Colex (∀ i, α i)` is a linear order if the original order has well-founded `>`. -/
noncomputable instance linearOrder [LinearOrder ι] [WellFoundedGT ι] [∀ a, LinearOrder (β a)] :
LinearOrder (Colex (∀ i, β i)) :=
Lex.linearOrder (ι := ιᵒᵈ)
