instCreatesLimitsOfShapeSheafPresheafForgetOfHasLimitsOfShape

Mathlib.Topology.Sheaves.Limits

URI: https://scilib.ai/kg/mathlib#TopCat.instCreatesLimitsOfShapeSheafPresheafForgetOfHasLimitsOfShape

Lean4

instance [HasLimitsOfShape J C] (X : TopCat.{t}) : CreatesLimitsOfShape J (Sheaf.forget C X) :=
  Sheaf.createsLimitsOfShape

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

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

Разделы

Аффилиация

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