instPartialOrder — Mathlib

English

There is a PartialOrder on α ⊕ β defined by lifting the componentwise order; antisymmetry holds and respects LiftRel.

Русский

На α ⊕ β задан частичный порядок, полученный подъёмом компонентного порядка; выполняется антисимметрия и он согласован с LiftRel.

LaTeX

$$$\text{PartialOrder}(\alpha \oplus \beta)$ with le_antisymm defined via LiftRel$$

Lean4

instance [PartialOrder α] [PartialOrder β] : PartialOrder (α ⊕ β) :=
  { instPreorderSum with le_antisymm := fun _ _ => show LiftRel _ _ _ _ → _ from antisymm }

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