topCat_hasLimitsOfShape — Mathlib

English

For any small category J, TopCat has limits of shape J; i.e., HasLimitsOfShape J TopCat.

Русский

Для любой малой категории J у TopCat существуют пределы формы J; то есть HasLimitsOfShape J TopCat.

LaTeX

$$$ HasLimitsOfShape\, J\, TopCat $$$

Lean4

instance topCat_hasLimitsOfShape (J : Type v) [Category J] [Small.{u} J] : HasLimitsOfShape J TopCat.{u} where
  has_limit := fun F => by
    rw [hasLimit_iff_small_sections]
    infer_instance

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