Comp

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

Statistics

Metric	Count
Definitions effectiveEpiFamilyStructCompIso, effectiveEpiFamilyStructCompOfEffectiveEpiSplitEpi, effectiveEpiFamilyStructCompOfEffectiveEpiSplitEpi', effectiveEpiFamilyStructOfComp	4
Theorems effectiveEpiFamilyStructCompIso_aux, effectiveEpiFamily_of_effectiveEpi_epi_comp, effectiveEpi_of_effectiveEpi_epi_comp, instEffectiveEpiFamilyComp, instEffectiveEpiFamilyCompOfIsSplitEpi	5
Total	9

CategoryTheory

Definitions

Name	Category	Theorems
effectiveEpiFamilyStructCompIso 📖	CompOp	—
effectiveEpiFamilyStructCompOfEffectiveEpiSplitEpi 📖	CompOp	—
effectiveEpiFamilyStructCompOfEffectiveEpiSplitEpi' 📖	CompOp	—
effectiveEpiFamilyStructOfComp 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
effectiveEpiFamilyStructCompIso_aux 📖	—	CategoryStruct.comp Category.toCategoryStruct	—	—	—
effectiveEpiFamily_of_effectiveEpi_epi_comp 📖	mathematical	Epi	EffectiveEpiFamily	—	—
effectiveEpi_of_effectiveEpi_epi_comp 📖	mathematical	—	EffectiveEpi	—	effectiveEpi_iff_effectiveEpiFamily effectiveEpiFamily_of_effectiveEpi_epi_comp instEffectiveEpiOfEffectiveEpiFamily
instEffectiveEpiFamilyComp 📖	mathematical	—	EffectiveEpiFamily CategoryStruct.comp Category.toCategoryStruct	—	—
instEffectiveEpiFamilyCompOfIsSplitEpi 📖	mathematical	IsSplitEpi	EffectiveEpiFamily CategoryStruct.comp Category.toCategoryStruct	—	—

---

← Back to Index