colim_preservesLimitsOfShape_pempty_of_isSifted

Mathlib.CategoryTheory.Limits.Sifted

URI: https://scilib.ai/kg/mathlib#CategoryTheory.IsSifted.colim_preservesLimitsOfShape_pempty_of_isSifted

← MathLib Explorer

English

Reiteration: IsSifted C iff IsSifted (AsSmall C).

Русский

Повтор: IsSifted C эквивалентно IsSifted (AsSmall C).

LaTeX

$$IsSifted C ⇔ IsSifted (AsSmall C)$$

Lean4

instance colim_preservesLimitsOfShape_pempty_of_isSifted :
    PreservesLimitsOfShape (Discrete PEmpty.{1}) (colim : (C ⥤ _) ⥤ Type u) :=
  preservesLimitsOfShape_pempty_of_preservesTerminal _

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

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

Разделы

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

Аффилиация

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