English
If X κ-presentable and F is an equivalence, then F.obj X is κ-presentable.
Русский
Если X κ-представим и F является эквивалентностью, то F.obj X κ-представим.
LaTeX
$$$[IsCardinalPresentable X \kappa] \Rightarrow IsCardinalPresentable (F.obj X) \kappa$$$
Lean4
theorem preservesColimitsOfShape_of_isCardinalPresentable_of_essentiallySmall [IsCardinalPresentable X κ] (J : Type u₃)
[Category.{v₃} J] [EssentiallySmall.{w} J] [IsCardinalFiltered J κ] :
PreservesColimitsOfShape J (coyoneda.obj (op X)) :=
(coyoneda.obj (op X)).preservesColimitsOfShape_of_isCardinalAccessible_of_essentiallySmall κ J
