Theorems · Theorem · category theory

CategoryTheory.IsCofiltered.cone_nonempty

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofiltered C] {J : Type w}
  [inst_2 : CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] (F : CategoryTheory.Functor J C),
  Nonempty (CategoryTheory.Limits.Cone F)

If we have IsCofiltered C, then for any functor F : J ⥤ C with FinCategory J, there exists a cone over F.

Defined in

Mathlib.CategoryTheory.Filtered.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.IsCofilteredCategoryTheory.SmallCategoryCategoryTheory.FinCategory