English
If ι is a LinearOrder, WellFoundedGT, and Nonempty, and each β i is a partial order with NoMaxOrder, then Colex (∀ i, β i) has NoMaxOrder.
Русский
Если ι — линейный порядок, WellFoundedGT и не пуст, и для каждого i β i — частично упорядованное множество без максимального элемента, тогда Colex (∀ i, β i) имеет NoMaxOrder.
LaTeX
$$$[\text{LinearOrder } \iota] \land [\text{WellFoundedGT } \iota] \land [\text{Nonempty } \iota] \land [\forall i, \ PartialOrder(\beta i)] \land [\forall i, \ NoMaxOrder(\beta i)] \Rightarrow NoMaxOrder(\mathrm{Colex}(\forall i,\beta i))$$$
Lean4
theorem noMaxOrder' [Preorder ι] [∀ i, LT (β i)] (i : ι) [NoMaxOrder (β i)] : NoMaxOrder (Colex (∀ i, β i)) :=
Lex.noMaxOrder' (ι := ιᵒᵈ) i
