has_limits_of_shape

Mathlib.CategoryTheory.Limits.HasLimits

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

← MathLib Explorer

English

Given a category C with limits, for any shape J, C has all limits of shape J; i.e., HasLimitsOfShape J C.

Русский

Если у C есть пределы, то у C есть пределы любой формы J; т.е. HasLimitsOfShape J C.

LaTeX

$$$\\text{HasLimitsOfShape } J\\; C$$$

Lean4

theorem has_limits_of_shape {C : Type u} [Category.{v} C] [HasLimits C] (J : Type v) [Category.{v} J] :
    HasLimitsOfShape J C :=
  HasLimitsOfSize.has_limits_of_shape J

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

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

Разделы

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

Аффилиация

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