English
The lexicographic order on Lex is densely ordered when the base is densely ordered, and the fibers are nonempty and densely ordered.
Русский
Лексикографический порядок denselyOrdered, когда база densely ordered, волокна непусты и densely ordered.
LaTeX
$$$\text{DenselyOrdered}(\Sigma_\text{Lex} i, α(i))$$$
Lean4
instance denselyOrdered [Preorder ι] [DenselyOrdered ι] [∀ i, Nonempty (α i)] [∀ i, Preorder (α i)]
[∀ i, DenselyOrdered (α i)] : DenselyOrdered (Σₗ i, α i) where
dense := 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⟩
