English
The sum α ⊕ β is densely ordered if and only if both α and β are densely ordered.
Русский
Сумма α ⊕ β плотно упорядочена тогда и только тогда, когда оба множества α и β плотно упорядочены.
LaTeX
$$$\text{DenselyOrdered}(\alpha \oplus \beta) \iff (\text{DenselyOrdered}(\alpha) \wedge \text{DenselyOrdered}(\beta))$$$
Lean4
@[simp]
theorem denselyOrdered_iff [LT α] [LT β] : DenselyOrdered (α ⊕ β) ↔ DenselyOrdered α ∧ DenselyOrdered β :=
⟨fun _ =>
⟨⟨fun a b h => by
obtain ⟨c | c, ha, hb⟩ := @exists_between (α ⊕ β) _ _ _ _ (inl_lt_inl_iff.2 h)
· exact ⟨c, inl_lt_inl_iff.1 ha, inl_lt_inl_iff.1 hb⟩
· exact (not_inl_lt_inr ha).elim⟩,
⟨fun a b h => by
obtain ⟨c | c, ha, hb⟩ := @exists_between (α ⊕ β) _ _ _ _ (inr_lt_inr_iff.2 h)
· exact (not_inl_lt_inr hb).elim
· exact ⟨c, inr_lt_inr_iff.1 ha, inr_lt_inr_iff.1 hb⟩⟩⟩,
fun h => @Sum.denselyOrdered _ _ _ _ h.1 h.2⟩
