noMinOrder_of_left — Mathlib

English

If α has NoMinOrder, then α × β has NoMinOrder for Preorder β.

Русский

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

LaTeX

$$$\forall \alpha \beta\,[\text{Preorder}(\alpha) \land \text{Preorder}(\beta) \land \text{NoMinOrder}(\alpha) \Rightarrow \text{NoMinOrder}(\alpha \times \beta)]$$$

Lean4

instance noMinOrder_of_left [Preorder α] [Preorder β] [NoMinOrder α] : NoMinOrder (α × β) :=
  ⟨fun ⟨a, b⟩ => by
    obtain ⟨c, h⟩ := exists_lt a
    exact ⟨(c, b), Prod.mk_lt_mk_iff_left.2 h⟩⟩

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