Theorems · Theorem · category theory

CategoryTheory.IsCofiltered.wideCospan

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] {I : Type u_1}
  [Finite I] {i : C} {j : I → C} (f : (x : I) → j x ⟶ i),
  ∃ k fki g, ∀ (x : I), CategoryTheory.CategoryStruct.comp (g x) (f x) = fki

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.IsCofilteredOrEmptyFinite