instPreservesLimitsOfSizeOfIsRightAdjoint

Mathlib.CategoryTheory.Adjunction.Limits

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

English

If F is a right adjoint, it preserves limits of size {v, u}.

Русский

Если F — правый сопряжённый, он сохраняет пределы размера {v, u}.

LaTeX

$$$$[\\text{IsRightAdjoint } F] \\Rightarrow \\operatorname{PreservesLimitsOfSize}.{v, u}\\; F.$$$$

Lean4

noncomputable instance [IsRightAdjoint F] : PreservesLimitsOfSize.{v, u} F where

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

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

Разделы

Аффилиация

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