limitsOfShape

Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ObjectProperty.LimitOfShape.limitsOfShape

English

If P has a limit of shape J at X, then P.limitsOfShape J X holds.

Русский

Если у P существует предел формы J в объекте X, то выполняется свойство limitsOfShape J X.

LaTeX

$$$P.\mathrm{LimitOfShape}(J,X) \Rightarrow P.\mathrm{limitsOfShape}(J,X)$$$

Lean4

theorem limitsOfShape {X : C} (h : P.LimitOfShape J X) : P.limitsOfShape J X :=
  ⟨h⟩

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

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

Разделы

Аффилиация

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