hasForgetToPartOrd — Mathlib

English

There is a forgetful functor from SemilatSupCat to PartOrd which preserves the lattice structure under the underlying order.

Русский

Существет забывающий функтор из SemilatSupCat в PartOrd, сохраняющий решётку подлежащей структуры порядка.

LaTeX

$$$\\text{forget to PartOrd} : \\mathrm{SemilatSupCat} \\to \\mathrm{PartOrd}$ is a forgetful functor.$$

Lean4

instance hasForgetToPartOrd : HasForget₂ SemilatInfCat PartOrd
    where
  forget₂.obj X := .of X
  forget₂.map f := PartOrd.ofHom ⟨f.toInfHom, OrderHomClass.mono f.toInfHom⟩

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