noMaxOrder_of_left — Mathlib

English

If α and β are Preorder, and α has NoMaxOrder, then α × β has NoMaxOrder.

Русский

Если α и β заданы частично упорядоченными, и в α нет максимума, то в произведении α × β нет максимума.

LaTeX

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

Lean4

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

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