English
If α and β are ordered and have no minimal element (NoMinOrder α and NoMinOrder β), then their sum α ⊕ β has no minimal element. Equivalently, neither α nor β has a least element implies α ⊕ β has no least element.
Русский
Если α и β упорядочены и в них нет минимального элемента, то их сумма α ⊕ β не имеет минимального элемента.
LaTeX
$$$\text{NoMinOrder}(\alpha \oplus \beta) \iff (\text{NoMinOrder}(\alpha) \wedge \text{NoMinOrder}(\beta))$$$
Lean4
@[simp]
theorem noMinOrder_iff [LT α] [LT β] : NoMinOrder (α ⊕ β) ↔ NoMinOrder α ∧ NoMinOrder β :=
⟨fun _ =>
⟨⟨fun a => by
obtain ⟨b | b, h⟩ := exists_lt (inl a : α ⊕ β)
· exact ⟨b, inl_lt_inl_iff.1 h⟩
· exact (not_inr_lt_inl h).elim⟩,
⟨fun a => by
obtain ⟨b | b, h⟩ := exists_lt (inr a : α ⊕ β)
· exact (not_inl_lt_inr h).elim
· exact ⟨b, inr_lt_inr_iff.1 h⟩⟩⟩,
fun h => @Sum.noMinOrder _ _ _ _ h.1 h.2⟩
