instIsFilteredDiscretePUnit

Mathlib.CategoryTheory.Filtered.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.instIsFilteredDiscretePUnit

← MathLib Explorer

English

The discrete one-point category is filtered.

Русский

Дискретная одноэлементная категория фильтрована.

LaTeX

$$$IsFiltered(Discrete PUnit)$$$

Lean4

instance : IsFiltered (Discrete PUnit)
    where
  cocone_objs X Y := ⟨⟨PUnit.unit⟩, ⟨⟨by trivial⟩⟩, ⟨⟨by subsingleton⟩⟩, trivial⟩
  cocone_maps X Y f g := ⟨⟨PUnit.unit⟩, ⟨⟨by trivial⟩⟩, by subsingleton⟩

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

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

Разделы

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

Аффилиация

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