coyonedaPreservesLimitsOfShape — Mathlib

English

For all X in Cᵒᵖ, the functor yonedaPreservesLimitsOfShape ensures that yoneda.obj X preserves limits of any shape J.

Русский

Для каждого X в Cᵒᵖ функтор yoneda.obj X сохраняет пределы любой формы J.

LaTeX

$$$\\forall X:\\, C^{op},\\; \\mathrm{PreservesLimitsOfShape}\\; (\\mathrm{yoneda.obj} X)$$$

Lean4

noncomputable instance coyonedaPreservesLimitsOfShape (X : Cᵒᵖ) : PreservesLimitsOfShape J (coyoneda.obj X) where

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