latToBddLat

Mathlib.Order.Category.BddLat

URI: https://scilib.ai/kg/mathlib#latToBddLat

Lean4

/-- The functor that adds a bottom and a top element to a lattice. This is the free functor. -/
def latToBddLat : Lat.{u} ⥤ BddLat where
  obj X := .of <| WithTop <| WithBot X
  map f := BddLat.ofHom <| LatticeHom.withTopWithBot f.hom

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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