Theorems · Theorem · category theory

CategoryTheory.Limits.hasCoproductsOfShape_of_small

∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (β : Type w₂) [Small.{w₁, w₂} β]
  [CategoryTheory.Limits.HasCoproducts C], CategoryTheory.Limits.HasCoproductsOfShape β C

Defined in: Mathlib.CategoryTheory.Limits.EssentiallySmall
Cited by: 1 results in Mathlib
Foundations: Depth 39 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CategoryTheory.Category Small CategoryTheory.Limits.HasCoproducts

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites8

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CategoryTheory.Categorystatement and proof · cited by 32,673
Equiv.symmproof · cited by 3,681
Smallstatement and proof · cited by 369
CategoryTheory.Limits.HasCoproductsstatement and proof · cited by 119
equivShrinkproof · cited by 118
CategoryTheory.Discrete.equivalenceproof · cited by 33
CategoryTheory.Limits.HasCoproductsOfShapestatement · cited by 29
CategoryTheory.Limits.hasColimitsOfShape_of_equivalenceproof · cited by 22

Cited by1

Results whose statement or proof uses this declaration.

CategoryTheory.ObjectProperty.isStrongGenerator_iff_exists_extremalEpiproof · cited by 0