noMaxOrder_of_right — Mathlib

English

If α is Preorder and β is Preorder with NoMaxOrder, then Lex(α × β) has no maximum element.

Русский

Если α — предобразованный порядок, β — предобразованный порядок с отсутствием максимума, то Lex(α × β) не имеет максимального элемента.

LaTeX

$$$\\text{NoMaxOrder}(\\mathrm{Lex}(\\alpha \\times \\beta))$ under $[\\text{Preorder }\\alpha], [\\text{Preorder }\\beta], [\\text{NoMaxOrder }\\beta].$$$

Lean4

instance noMaxOrder_of_right [Preorder α] [Preorder β] [NoMaxOrder β] : NoMaxOrder (α ×ₗ β) where
  exists_gt := by
    rintro ⟨a, b⟩
    obtain ⟨c, h⟩ := exists_gt b
    exact ⟨⟨a, c⟩, right _ h⟩

Похожие утверждения