lim_preservesLimits — Mathlib

English

The limit functor preserves all limits, i.e., limits commute with taking limits over shapes.

Русский

Функтор предела сохраняет все пределы: пределы коммутируют с взятием пределов по формам.

LaTeX

$$$$ \\text{PreservesLimits}(\\mathrm{lim})$$$$

Lean4

instance lim_preservesLimits [HasLimitsOfShape J C] : PreservesLimits (lim (J := J) (C := C)) :=
  constLimAdj.rightAdjoint_preservesLimits

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