English
The lexicographical order on Lex has a top element given by (⊤, ⊤) when the index ι has a top and each fiber α(i) has a top element.
Русский
Лексикографический порядок имеет верхнюю границу, равную (⊤, ⊤), если в индексе ι существует верхняя граница, а в каждой волокне α(i) есть верхний элемент.
LaTeX
$$$\text{top} = (\top, \top)$ and $x \le \text{top}$ for all x in Lex.$$
Lean4
/-- The lexicographical linear order on a sigma type. -/
instance orderTop [PartialOrder ι] [OrderTop ι] [∀ i, Preorder (α i)] [OrderTop (α ⊤)] : OrderTop (Σₗ i, α i)
where
top := ⟨⊤, ⊤⟩
le_top := fun ⟨a, b⟩ => by
obtain rfl | ha := eq_top_or_lt_top a
· exact Lex.right _ _ le_top
· exact Lex.left _ _ ha
