English
If α and β are densely ordered with NoMinOrder on β, and α is densely ordered as well, then α ⊕ₗ β is densely ordered; density follows from exists_between and exists_lt in the left and right components.
Русский
Если α и β плотны и β имеет NoMinOrder, то сумма Lex плотна; плотность достигается через exists_between и exists_lt.
LaTeX
$$$\\text{DenselyOrdered}(\\alpha ⊕_ℓ β)$ under NoMinOrder on β$$
Lean4
instance denselyOrdered_of_noMinOrder [LT α] [LT β] [DenselyOrdered α] [DenselyOrdered β] [NoMinOrder β] :
DenselyOrdered (α ⊕ₗ β) :=
⟨fun a b h =>
match a, b, h with
| inl _, inl _, Lex.inl h =>
let ⟨c, ha, hb⟩ := exists_between h
⟨toLex (inl c), inl_lt_inl_iff.2 ha, inl_lt_inl_iff.2 hb⟩
| inl _, inr b, Lex.sep _ _ =>
let ⟨c, h⟩ := exists_lt b
⟨toLex (inr c), inl_lt_inr _ _, inr_lt_inr_iff.2 h⟩
| inr _, inr _, Lex.inr h =>
let ⟨c, ha, hb⟩ := exists_between h
⟨toLex (inr c), inr_lt_inr_iff.2 ha, inr_lt_inr_iff.2 hb⟩⟩
