English
If α is nonempty and has LT with NoMinOrder, then α ⊕ₗ β also has NoMinOrder; nonemptiness of α ensures a witness in the left or right component.
Русский
Если α непусто и имеет NoMinOrder, то α ⊕ₗ β тоже имеет NoMinOrder; непустота α гарантирует существование минимального в одном из компонентов.
LaTeX
$$$\\text{NoMinOrder}(\\alpha \\oplus_ℓ \\beta)$ under NoMinOrder and nonempty α$$
Lean4
instance noMaxOrder [LT α] [LT β] [NoMaxOrder α] [NoMaxOrder β] : NoMaxOrder (α ⊕ₗ β) :=
⟨fun a =>
match a with
| inl a =>
let ⟨b, h⟩ := exists_gt a
⟨toLex (inl b), inl_lt_inl_iff.2 h⟩
| inr a =>
let ⟨b, h⟩ := exists_gt a
⟨toLex (inr b), inr_lt_inr_iff.2 h⟩⟩
