English
The lexicographic order on Σₗ' i, α i has a bottom element given by (⊥, ⊥), which is below every element of the sigma-type.
Русский
Лексикографический порядок на Σₗ' i, α_i имеет нижний элемент ⊥, который лежит ниже любого элемента сигма-типа.
LaTeX
$$$\\text{bot} = (\\bot,\\bot)$ and ∀ x, \\text{bot} \\le_{\\mathrm{Lex}} x$$
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
