instNoMaxOrderColexForallOfWellFoundedGTOfNonempty

English

If ι is LinearOrder with WellFoundedGT and Nonempty, and each β i is a partial order with NoMaxOrder, then Colex (∀ i, β i) has NoMaxOrder.

Русский

Если ι — линейный порядок с WellFoundedGT и непуст, и каждый β i частично упорядован и не имеет максимального элемента, то Colex (∀ i, β i) не имеет максимального элемента.

LaTeX

$$$[\text{LinearOrder } ι] \land [\text{WellFoundedGT } ι] \land [\text{Nonempty } ι] \land [\forall i, \ PartialOrder(β i)] \land [\forall i, NoMaxOrder(β i)] \Rightarrow NoMaxOrder(\mathrm{Colex}(\forall i,β i))$$$

Lean4

instance [LinearOrder ι] [WellFoundedGT ι] [Nonempty ι] [∀ i, PartialOrder (β i)] [∀ i, NoMaxOrder (β i)] :
    NoMaxOrder (Colex (∀ i, β i)) :=
  inferInstanceAs (NoMaxOrder (Lex (∀ i : ιᵒᵈ, β (OrderDual.toDual i))))

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