instNoMaxOrderLexForallOfWellFoundedLTOfNonempty

English

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

Русский

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

LaTeX

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

Lean4

instance [LinearOrder ι] [WellFoundedLT ι] [Nonempty ι] [∀ i, PartialOrder (β i)] [∀ i, NoMaxOrder (β i)] :
    NoMaxOrder (Lex (∀ i, β i)) :=
  ⟨fun a =>
    let ⟨_, hb⟩ := exists_gt (ofLex a)
    ⟨_, toLex_strictMono hb⟩⟩

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