Commit 2024-02-27 23:07 fca284d1

View on Github →

feat(Topology/Category): EffectiveEpi iff QuotientMap in TopCat (#10993)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Category/TopCat/EffectiveEpi.lean

added def TopCat.effectiveEpiStructOfQuotientMap

added theorem TopCat.effectiveEpi_iff_quotientMap