Theorems · Theorem · category theory

CategoryTheory.Limits.HasCofilteredLimitsOfSize.HasLimitsOfShape

∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C}
  [self : CategoryTheory.Limits.HasCofilteredLimitsOfSize.{w', w, v, u} C] (I : Type w)
  [inst_1 : CategoryTheory.Category.{w', w} I] [CategoryTheory.IsCofiltered I],
  CategoryTheory.Limits.HasLimitsOfShape I C

For all filtered types of size w, we have limits

Defined in

Mathlib.CategoryTheory.Limits.Filtered

Cited by

0 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

CategoryTheory.Limits.HasCofilteredLimitsOfSizeCategoryTheory.CategoryCategoryTheory.IsCofiltered