opHomOfLE — Mathlib

English

From an inequality in X, construct a morphism in the opposite category X^op from y to x.

Русский

Из неравенства в X строится морфизм в противоположной категории X^op от y к x.

LaTeX

$$$\mathrm{opHomOfLE} : \{x,y : X^{\mathrm{op}}\} \to (unop\,x \le unop\,y) \to y \to x$ is given by $\mathrm{opHomOfLE}(h) = (\mathrm{homOfLE}(h)).\mathrm{op}$.$$

Lean4

/-- Construct a morphism in the opposite of a preorder category from an inequality. -/
def opHomOfLE {x y : Xᵒᵖ} (h : unop x ≤ unop y) : y ⟶ x :=
  (homOfLE h).op

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