toOrderHom — Mathlib

English

A functor F: X ⥤ Y gives an order-hom X →o Y with toFun = F.obj and monotone' = F.monotone.

Русский

Функтор F: X ⥤ Y задаёт отображение по порядку X →o Y с toFun = F.obj и монотонностью, равной F.monotone.

LaTeX

$$\text{toOrderHom}(F) : X \too Y$$

Lean4

/-- A functor `X ⥤ Y` between preorder categories as an `OrderHom`. -/
@[simps!]
def toOrderHom (F : X ⥤ Y) : X →o Y where
  toFun := F.obj
  monotone' := F.monotone

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