noMaxOrder_of_nonempty — Mathlib

English

If α is nonempty and NoMaxOrder on β holds, then the Lex-ordered sum α ⊕ₗ β has NoMaxOrder; symmetric statements hold for nonempty β.

Русский

Если β непусто и NoMaxOrder на β, то сумма Lex имеет NoMaxOrder; аналогично для α.

LaTeX

$$$\\text{NoMaxOrder}(\\alpha \\oplus_ℓ \\beta)$$$

Lean4

instance noMaxOrder_of_nonempty [LT α] [LT β] [NoMaxOrder β] [Nonempty β] : NoMaxOrder (α ⊕ₗ β) :=
  ⟨fun a =>
    match a with
    | inl _ => ⟨toLex (inr <| Classical.arbitrary β), inl_lt_inr _ _⟩
    | inr a =>
      let ⟨b, h⟩ := exists_gt a
      ⟨toLex (inr b), inr_lt_inr_iff.2 h⟩⟩

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