hasForgetToSemilatInf — Mathlib

English

There exists a forgetful functor from BddLat to SemilatInfCat, i.e., a mapping of bounded lattices to semilattices with a meet operation via forgetting structure.

Русский

Существует забывающий функтор из BddLat в SemilatInfCat, переводящий ограниченную решетку в полупропессивную структуру, забывая операцию meet.

LaTeX

$$\\text{HasForget}_2\, BddLat \\; SemilatInfCat$$

Lean4

instance hasForgetToSemilatInf : HasForget₂ BddLat SemilatInfCat
    where
  forget₂.obj X := .of X
  forget₂.map f := f.hom.toInfTopHom

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