hasForgetToLat

Mathlib.Order.Category.Frm

URI: https://scilib.ai/kg/mathlib#Frm.hasForgetToLat

English

There is a forgetful functor from Frm to Lat, sending a frame X to Lat.of X and a morphism to its Lat-hom.

Русский

Существуют забывательные функторы Frm → Lat, отправляющие рамку X в Lat.of X и морфизм в Lat-гом.

LaTeX

$$HasForget₂ Frm Lat$$

Lean4

instance hasForgetToLat : HasForget₂ Frm Lat where
  forget₂.obj X := .of X
  forget₂.map f := Lat.ofHom f.hom

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru