instIsPresentableObjJDiagColimitPresentation

English

For every j in the indexing J X, the diagonal presentation object (h.colimitPresentation X).diag.obj j is presentable.

Русский

Для каждого j из индекса J X диагональный презентационный объект (h.colimitPresentation X).diag.obj j презентируем.

LaTeX

$$$\forall j : h.J X,\ IsPresentable((h.colimitPresentation X).diag.obj j)$$$

Lean4

instance (j : h.J X) : IsPresentable.{w} ((h.colimitPresentation X).diag.obj j) :=
  isPresentable_of_isCardinalPresentable _ κ

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