noMinOrder — Mathlib

English

If either α or β has no minimal element, then the Lex-ordered sum α ⊕ₗ β has no minimal element as well; explicit witnesses can be given by inl/inr using exists_lt.

Русский

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

LaTeX

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

Lean4

instance noMinOrder [LT α] [LT β] [NoMinOrder α] [NoMinOrder β] : NoMinOrder (α ⊕ₗ β) :=
  ⟨fun a =>
    match a with
    | inl a =>
      let ⟨b, h⟩ := exists_lt a
      ⟨toLex (inl b), inl_lt_inl_iff.2 h⟩
    | inr a =>
      let ⟨b, h⟩ := exists_lt a
      ⟨toLex (inr b), inr_lt_inr_iff.2 h⟩⟩

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