evaluationPreservesLimitsOfSize

Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits

URI: https://scilib.ai/kg/mathlib#SheafOfModules.evaluationPreservesLimitsOfSize

← MathLib Explorer

English

For each X, the evaluation Ev_X preserves limits of any size.

Русский

Для каждого X операция оценки сохраняет пределы любого размера.

LaTeX

$$$\operatorname{PreservesLimitsOfSize}(\mathrm{Ev}_X)$$$

Lean4

noncomputable instance evaluationPreservesLimitsOfSize (X : Cᵒᵖ) :
    PreservesLimitsOfSize.{v₂, v} (evaluation R X : SheafOfModules.{v} R ⥤ _) where

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

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

Разделы

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

Аффилиация

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