English
If α and β are densely ordered, then the sum α ⊕ β, endowed with the lexicographic-type order, is densely ordered.
Русский
Если α и β плотно упорядочены, то сумма α ⊕ β, снабжённая лексикографическим порядком по пару, является плотно упорядоченной.
LaTeX
$$$\text{DenselyOrdered}(\alpha \oplus \beta)$ при $[LT]\α$, $[LT]\β$, $\text{DenselyOrdered}(\alpha)$ и $\text{DenselyOrdered}(\beta)$.$$
Lean4
instance denselyOrdered [LT α] [LT β] [DenselyOrdered α] [DenselyOrdered β] : DenselyOrdered (α ⊕ β) :=
⟨fun a b h =>
match a, b, h with
| inl _, inl _, LiftRel.inl h =>
let ⟨c, ha, hb⟩ := exists_between h
⟨toLex (inl c), LiftRel.inl ha, LiftRel.inl hb⟩
| inr _, inr _, LiftRel.inr h =>
let ⟨c, ha, hb⟩ := exists_between h
⟨toLex (inr c), LiftRel.inr ha, LiftRel.inr hb⟩⟩
