Theorems · Theorem · category theory

CategoryTheory.ObjectProperty.of_essentiallySmall_index

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {X : C} {J : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.EssentiallySmall.{w, v_1, u_1} J]
  [CategoryTheory.IsFiltered J] (pres : CategoryTheory.Limits.ColimitPresentation J X),
  (∀ (i : J), P (pres.diag.obj i)) → P.ind X

Defined in

Mathlib.CategoryTheory.ObjectProperty.Ind

Cited by

1 results in Mathlib

Foundations

Depth 45 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.EssentiallySmallCategoryTheory.IsFiltered