instPreorder — Mathlib

English

For an ordered type α, the opposite type αᵐᵒᵖ carries the induced preorder obtained by applying the unop map: a ≤ b in αᵐᵒᵖ iff unop a ≤ unop b in α.

Русский

У противоположного типа αᵐᵒᵖ имеется индуцированный порядок, получаемый через отображение unop: a ≤ b в αᵐᵒᵖ эквивалентно unop a ≤ unop b в α.

LaTeX

$$$\text{Preorder}(\alpha^{\mathrm{op}}) \text{ is given by } a \le b \iff a^{\mathrm{unop}} \le b^{\mathrm{unop}}$.$$

Lean4

@[to_additive]
instance : Preorder αᵐᵒᵖ :=
  Preorder.lift unop

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