English
Assume a Preorder ι, and that each β i is linearly ordered (LT) and densely ordered. Then the lexicographic order on the dependent product ∀ i, β i is densely ordered.
Русский
Пусть имеется предпорядок ι и для каждого i выполняется LT и плотность порядка в β i. Тогда лексикографический порядок на произведении ∀ i, β i является плотно упорядоченным.
LaTeX
$$$[\text{Preorder } \iota] \land [\forall i, \ LT(\beta i)] \land [\forall i, \ DenselyOrdered(\beta i)] \Rightarrow \ DenselyOrdered(\mathrm{Lex}(\forall i,\beta i))$$$
Lean4
instance [Preorder ι] [∀ i, LT (β i)] [∀ i, DenselyOrdered (β i)] : DenselyOrdered (Lex (∀ i, β i)) :=
⟨by
rintro _ a₂ ⟨i, h, hi⟩
obtain ⟨a, ha₁, ha₂⟩ := exists_between hi
classical
refine ⟨Function.update a₂ _ a, ⟨i, fun j hj => ?_, ?_⟩, i, fun j hj => ?_, ?_⟩
· rw [h j hj]
dsimp only at hj
rw [Function.update_of_ne hj.ne a]
· rwa [Function.update_self i a]
· rw [Function.update_of_ne hj.ne a]
· rwa [Function.update_self i a]⟩
