English
If α and β are types with a strict order ≤ and there is no maximal element in each (NoMaxOrder α and NoMaxOrder β), then the disjoint sum α ⊕ β, endowed with the standard sum order, has no maximal element. Specifically, for any element of α ⊕ β, there is a strictly larger element: if the element is inl a, pick b > a in α and take inl b; if the element is inr a, pick b > a in β and take inr b.
Русский
Если α и β упорядочены по отношению ≤ и в каждом из них нет максимального элемента, то их сумма α ⊕ β, на которой задан стандартный «суммарный» порядок, тоже не имеет максимального элемента. Для любого элемента из α ⊕ β существует больший элемент: если элемент равен inl a, возьмём b > a в α и возьмем inl b; если элемент равен inr a, возьмём b > a в β и возьмём inr b.
LaTeX
$$$\text{NoMaxOrder}(\alpha \oplus \beta)$ при $[LT\;\alpha]$, $[LT\;\beta]$, $\text{NoMaxOrder}(\alpha)$ и $\text{NoMaxOrder}(\beta)$. Иными словами, для каждого элемента суммы существует элемент больший его; если элемент $\mathrm{inl}(a)$, берём $\mathrm{inl}(b)$ с $a < b$ в $\alpha$; если элемент $\mathrm{inr}(a)$, берём $\mathrm{inr}(b)$ с $a < b$ в $\beta$.$$
Lean4
instance noMaxOrder [LT α] [LT β] [NoMaxOrder α] [NoMaxOrder β] : NoMaxOrder (α ⊕ β) :=
⟨fun a =>
match a with
| inl a =>
let ⟨b, h⟩ := exists_gt a
⟨inl b, inl_lt_inl_iff.2 h⟩
| inr a =>
let ⟨b, h⟩ := exists_gt a
⟨inr b, inr_lt_inr_iff.2 h⟩⟩
