yoneda_preservesLimitsOfShape — Mathlib

English

For any diagram shape J, the functor yoneda.obj X preserves limits of shape J for any X in C.

Русский

Для любой формы диаграммы J отображение yoneda.obj X сохраняет пределы формы J для любого X ∈ C.

LaTeX

$$$\\forall J,\\; \\mathrm{PreservesLimitsOfShape}\\! J\\ (\\mathrm{yoneda.obj} X)$$$

Lean4

noncomputable instance yoneda_preservesLimitsOfShape (X : C) : PreservesLimitsOfShape J (yoneda.obj X) where

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