Commit 2024-02-17 16:15 fd9854c4

View on Github →

feat(CategoryTheory): equivalences of categories preserve effective epis (#10421)

Estimated changes

Modified Mathlib/CategoryTheory/Equivalence.lean

Modified Mathlib/CategoryTheory/Sites/EffectiveEpimorphic.lean

added def CategoryTheory.effectiveEpiFamilyStructCompIso

added theorem CategoryTheory.effectiveEpiFamilyStructCompIso_aux

added def CategoryTheory.effectiveEpiFamilyStructIsoComp

added theorem CategoryTheory.effectiveEpiFamilyStructIsoComp_aux

added def CategoryTheory.effectiveEpiFamilyStructOfEquivalence

added theorem CategoryTheory.effectiveEpiFamilyStructOfEquivalence_aux