noMinOrder_of_right — Mathlib

English

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

Русский

Если α — частично упорядоченное множество, β — с NoMinOrder, то Lex(α × β) не имеет минимума.

LaTeX

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

Lean4

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

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