Commit 2023-09-29 04:01 31679891

View on Github →

feat: a single element EffectiveEpiFamily consists of an EffectiveEpi (#7420)

Estimated changes

Modified Mathlib/CategoryTheory/Sites/EffectiveEpimorphic.lean

added def CategoryTheory.EffectiveEpiStruct_ofFamily

added theorem CategoryTheory.effectiveEpi_iff_effectiveEpiFamily