English
If α is a Preorder with NoMaxOrder and β is Preorder, then the lexicographic product Lex(α × β) also has no maximum element.
Русский
Если α — частично упорядоченное множество без максимального элемента, и β — частично упорядоченное множество, то лексикографическое произведение Lex(α × β) также не имеет максимального элемента.
LaTeX
$$$\\text{NoMaxOrder}(\\mathrm{Lex}(\\alpha \\times \\beta))$ under $[\\text{Preorder }\\alpha], [\\text{Preorder }\\beta], [\\text{NoMaxOrder }\\alpha].$$$
Lean4
instance noMaxOrder_of_left [Preorder α] [Preorder β] [NoMaxOrder α] : NoMaxOrder (α ×ₗ β) where
exists_gt := by
rintro ⟨a, b⟩
obtain ⟨c, h⟩ := exists_gt a
exact ⟨⟨c, b⟩, left _ _ h⟩
