English
The lexicographical order has a bottom element given by (⊥, ⊥), provided the base orders have bottom elements.
Русский
Лексикографический порядок имеет элемент-ниже всего, равный (⊥, ⊥), при условии существования нижних границ в базовых множествах.
LaTeX
$$$\text{bot} = (\bot, \bot)$ and $\text{bot} \le (i,a)$ for all $(i,a)$ in Lex.$$
Lean4
/-- The lexicographical linear order on a sigma type. -/
instance orderBot [PartialOrder ι] [OrderBot ι] [∀ i, Preorder (α i)] [OrderBot (α ⊥)] : OrderBot (Σₗ i, α i)
where
bot := ⟨⊥, ⊥⟩
bot_le := fun ⟨a, b⟩ => by
obtain rfl | ha := eq_bot_or_bot_lt a
· exact Lex.right _ _ bot_le
· exact Lex.left _ _ ha
