English
If α and β have LT with NoMinOrder, then α ⊕ β has NoMinOrder as well; every element has a smaller element in its component, yielding no minimal element in the sum.
Русский
Если α и β имеют LT с NoMinOrder, то и α ⊕ β имеет NoMinOrder; у каждого элемента есть меньший элемент в своей компоненте, поэтому в сумме нет наименьшего элемента.
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
⟨inl b, inl_lt_inl_iff.2 h⟩
| inr a =>
let ⟨b, h⟩ := exists_lt a
⟨inr b, inr_lt_inr_iff.2 h⟩⟩
