mathlib
e4ee4e30 - feat(category_theory/limits): colimits from finite colimits and filtered colimits (#16373)

Commit

3 years ago

feat(category_theory/limits): colimits from finite colimits and filtered colimits (#16373) We will use this in the future to show that if C has finite colimits, then Ind(C) is cocomplete.

Author

TwoFX

Parents

aa701d8f

mathlib e4ee4e30 - feat(category_theory/limits): colimits from finite colimits and filtered colimits (#16373)

mathlib
e4ee4e30 - feat(category_theory/limits): colimits from finite colimits and filtered colimits (#16373)