instPreorder — Mathlib

English

There is a natural Preorder on the product α × β given the Preorders on α and β, defined coordinatewise.

Русский

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

LaTeX

$$$\text{Preorder}(\alpha \times \beta)$ with$\; (a,b) \le (a',b') \iff a\le a' \land b\le b'.$$$

Lean4

instance : Preorder (α × β) where
  __ := inferInstanceAs (LE (α × β))
  le_refl := fun ⟨a, b⟩ ↦ ⟨le_refl a, le_refl b⟩
  le_trans := fun ⟨_, _⟩ ⟨_, _⟩ ⟨_, _⟩ ⟨hac, hbd⟩ ⟨hce, hdf⟩ ↦ ⟨le_trans hac hce, le_trans hbd hdf⟩

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