homOfLE — Mathlib

English

There is a canonical morphism from x to y in the preorder category whenever x ≤ y; it is denoted h.hom.

Русский

Существет каноническая стрелка от x к y в предельно-порядковой категории при условии x ≤ y; она обозначается h.hom.

LaTeX

$$$\mathrm{homOfLE} : \{X : Type\, u\} \to \{x,y : X\} \to (x \le y) \to (x \to y)$.$$

Lean4

/-- Express an inequality as a morphism in the corresponding preorder category. -/
def homOfLE {x y : X} (h : x ≤ y) : x ⟶ y :=
  ULift.up (PLift.up h)

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