corepresentable_preservesLimitsOfShape

Mathlib.CategoryTheory.Limits.Yoneda

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.corepresentable_preservesLimitsOfShape

English

For corepresentable F, corepresentablePreservesLimitsOfShape (J) holds; i.e., limits over shape J are preserved by F.

Русский

Для ядра F сохраняются пределы формы J; то есть F сохраняет пределы над формой J.

LaTeX

$$$\\mathrm{PreservesLimitsOfShape}\\; J\\ F$$$

Lean4

instance corepresentable_preservesLimitsOfShape : PreservesLimitsOfShape J F where

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

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

Разделы

Аффилиация

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