reflectsColimitsOfShape_subsingleton

Mathlib.CategoryTheory.Limits.Preserves.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.reflectsColimitsOfShape_subsingleton

← MathLib Explorer

English

For any J, ReflectsColimitsOfShape J F is a subsingleton.

Русский

Для любой J ReflectsColimitsOfShape J F является подсинглотоном.

LaTeX

$$$ \\operatorname{Subsingleton}(\\ReflectsColimitsOfShape J F). $$$

Lean4

instance reflectsColimitsOfShape_subsingleton (J : Type w) [Category.{w'} J] (F : C ⥤ D) :
    Subsingleton (ReflectsColimitsOfShape J F) := by constructor; rintro ⟨a⟩ ⟨b⟩; congr!

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

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

Разделы

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

Аффилиация

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