Theorems · Theorem · category theory

CategoryTheory.Limits.HasCountableLimits.out

∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} [self : CategoryTheory.Limits.HasCountableLimits C]
  (J : Type) [inst_1 : CategoryTheory.SmallCategory J] [CategoryTheory.CountableCategory J],
  CategoryTheory.Limits.HasLimitsOfShape J C

C has all limits over any type J whose objects and morphisms lie in the same universe and which has countably many objects and morphisms

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Countable

Cited by

0 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

CategoryTheory.Limits.HasCountableLimitsCategoryTheory.SmallCategoryCategoryTheory.CountableCategory