English
If α and β are ordered types with no maximal element, then α ⊕ β has no maximal element; equivalently, NoMaxOrder α ∧ NoMaxOrder β implies NoMaxOrder (α ⊕ β).
Русский
Если в α и β нет максимального элемента, то и в α ⊕ β тоже нет максимального элемента; равносильно тому, что NoMaxOrder α и NoMaxOrder β вместе эквивалентны NoMaxOrder (α ⊕ β).
LaTeX
$$$\text{NoMaxOrder}(\alpha \oplus \beta) \iff (\text{NoMaxOrder}(\alpha) \wedge \text{NoMaxOrder}(\beta))$$$
Lean4
@[simp]
theorem noMaxOrder_iff [LT α] [LT β] : NoMaxOrder (α ⊕ β) ↔ NoMaxOrder α ∧ NoMaxOrder β :=
⟨fun _ =>
⟨⟨fun a => by
obtain ⟨b | b, h⟩ := exists_gt (inl a : α ⊕ β)
· exact ⟨b, inl_lt_inl_iff.1 h⟩
· exact (not_inl_lt_inr h).elim⟩,
⟨fun a => by
obtain ⟨b | b, h⟩ := exists_gt (inr a : α ⊕ β)
· exact (not_inr_lt_inl h).elim
· exact ⟨b, inr_lt_inr_iff.1 h⟩⟩⟩,
fun h => @Sum.noMaxOrder _ _ _ _ h.1 h.2⟩
