noMaxOrder_of_right — 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}(\beta) \Rightarrow \text{NoMaxOrder}(\alpha \times \beta)]$$$

Lean4

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

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