Commit 2024-04-06 07:01 7c41b874

View on Github →

feat(CategoryTheory): a family is effective epi iff its precomposition with a family of split epis is (#11569)

Estimated changes

Modified Mathlib/CategoryTheory/EffectiveEpi/Comp.lean

added def CategoryTheory.effectiveEpiFamilyStructCompOfEffectiveEpiSplitEpi'

added def CategoryTheory.effectiveEpiFamilyStructCompOfEffectiveEpiSplitEpi

deleted def CategoryTheory.effectiveEpiFamilyStructIsoComp

deleted theorem CategoryTheory.effectiveEpiFamilyStructIsoComp_aux

added theorem CategoryTheory.effectiveEpiFamily_of_effectiveEpi_epi_comp

deleted def CategoryTheory.effectiveEpiStructCompOfEffectiveEpiSplitEpi'

deleted def CategoryTheory.effectiveEpiStructCompOfEffectiveEpiSplitEpi

added theorem CategoryTheory.effectiveEpi_of_effectiveEpi_epi_comp