Coproduct

📁 Source: Mathlib/CategoryTheory/EffectiveEpi/Coproduct.lean

Statistics

Metric	Count
Definitions effectiveEpiFamilyStructOfEffectiveEpiDesc, effectiveEpiStructIsColimitDescOfEffectiveEpiFamily	2
Theorems effectiveEpiFamilyStructOfEffectiveEpiDesc_aux, instEffectiveEpiDescOfEffectiveEpiFamily	2
Total	4

CategoryTheory

Definitions

Name	Category	Theorems
effectiveEpiFamilyStructOfEffectiveEpiDesc 📖	CompOp	—
effectiveEpiStructIsColimitDescOfEffectiveEpiFamily 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
effectiveEpiFamilyStructOfEffectiveEpiDesc_aux 📖	—	Limits.HasPullback Limits.sigmaObj Limits.Sigma.ι Limits.HasCoproduct Limits.pullback Epi Limits.Sigma.desc Limits.pullback.fst CategoryStruct.comp Category.toCategoryStruct	—	—	cancel_epi Limits.Sigma.hom_ext Limits.colimit.ι_desc_assoc Category.assoc Limits.pullback.condition Limits.colimit.ι_desc
instEffectiveEpiDescOfEffectiveEpiFamily 📖	mathematical	—	EffectiveEpi Limits.sigmaObj Limits.Sigma.desc	—	Category.id_comp

---

← Back to Index