instLE_mathlib — Mathlib

English

Let α and β be objects with a defined order. The Cartesian product α × β is ordered componentwise by (a1,b1) ≤ (a2,b2) iff a1 ≤ a2 and b1 ≤ b2.

Русский

Пусть заданы упорядоченные множества α и β. Произведение α × βlex упорядочено по компонентам: (a1,b1) ≤ (a2,b2) тогда и только тогда, когда a1 ≤ a2 и b1 ≤ b2.

LaTeX

$$$\forall x,y\in \alpha\times\beta,\; x\le y \;\iff\; x_1\le y_1 \land x_2\le y_2$$$

Lean4

instance : LE (α × β) where le p q := p.1 ≤ q.1 ∧ p.2 ≤ q.2

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