noMinOrder_of_nonempty — Mathlib

English

If either α or β lacks a maximal element, the Lex-ordered sum α ⊕ₗ β also lacks a maximal element; explicit witnesses obtained via inl or inr witness the nonexistence.

Русский

Если в одной из компонент нет максимального элемента, то и в лексикографической сумме нет максимального элемента.

LaTeX

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

Lean4

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

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