Commit 2024-04-04 13:54 f73c1a37

View on Github →

feat(CategoryTheory): define class ReflectsEffectiveEpis (#11476)

depends on: #11458

Estimated changes

Modified Mathlib/CategoryTheory/EffectiveEpi/Preserves.lean

added theorem CategoryTheory.Functor.effectiveEpiFamily_of_map

added theorem CategoryTheory.Functor.effectiveEpi_of_map

added theorem CategoryTheory.Functor.finite_effectiveEpiFamily_of_map