English
There is a pointwise partial order on α × β: if α and β are partially ordered, then (a1,b1) ≤ (a2,b2) iff a1 ≤ a2 and b1 ≤ b2, with antisymmetry given coordinatewise.
Русский
Существует точечный частичный порядок на произведении α × β: если α и β частично упорядочены, то (a1,b1) ≤ (a2,b2) тогда и только тогда a1 ≤ a2 и b1 ≤ b2, антисимметрия по координатам.
LaTeX
$$$\text{PartialOrder}(\alpha) \land \text{PartialOrder}(\beta) \Rightarrow \text{PartialOrder}(\alpha \times \beta)$ with$\; (a,b) \le (a',b') \iff a \le a' \land b \le b'.$$$
Lean4
/-- The pointwise partial order on a product.
(The lexicographic ordering is defined in `Order.Lexicographic`, and the instances are
available via the type synonym `α ×ₗ β = α × β`.) -/
instance instPartialOrder (α β : Type*) [PartialOrder α] [PartialOrder β] : PartialOrder (α × β)
where
__ := inferInstanceAs (Preorder (α × β))
le_antisymm := fun _ _ ⟨hac, hbd⟩ ⟨hca, hdb⟩ ↦ Prod.ext (hac.antisymm hca) (hbd.antisymm hdb)
