noMinOrder_of_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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