English
If ι is densely ordered and all α_i are densely ordered and nonempty, then the lexicographic sigma-type Σₗ' i, α_i is densely ordered.
Русский
Если ι упорядочено плотно и все α_i также плотно упорядочены и не пусты, то лексикографический сигма-тип Σₗ' i, α_i плотно упорядочен.
LaTeX
$$$\\text{DenselyOrdered}(\\Sigma'_i,\\alpha_i)$$$
Lean4
instance denselyOrdered [Preorder ι] [DenselyOrdered ι] [∀ i, Nonempty (α i)] [∀ i, Preorder (α i)]
[∀ i, DenselyOrdered (α i)] : DenselyOrdered (Σₗ' i, α i) :=
⟨by
rintro ⟨i, a⟩ ⟨j, b⟩ (⟨_, _, h⟩ | @⟨_, _, b, h⟩)
· obtain ⟨k, hi, hj⟩ := exists_between h
obtain ⟨c⟩ : Nonempty (α k) := inferInstance
exact ⟨⟨k, c⟩, left _ _ hi, left _ _ hj⟩
· obtain ⟨c, ha, hb⟩ := exists_between h
exact ⟨⟨i, c⟩, right _ ha, right _ hb⟩⟩
