instPreservesLimitEval

Mathlib.Algebra.Homology.HomologicalComplexLimits

URI: https://scilib.ai/kg/mathlib#HomologicalComplex.instPreservesLimitEval

← MathLib Explorer

English

For each i, the evaluation at i preserves limits of diagrams F: J ⥤ HomologicalComplex C c.

Русский

Для каждого i оценка в i сохраняет пределы диаграмм F: J ⥤ HomologicalComplex C c.

LaTeX

$$$ \forall n, \mathrm{PreservesLimit}(F, \mathrm{eval}_{n}). $$$

Lean4

noncomputable instance (n : ι) : PreservesLimit F (eval C c n) :=
  preservesLimit_of_preserves_limit_cone (isLimitConeOfHasLimitEval F) (limit.isLimit _)

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

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

Разделы

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

Аффилиация

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