Commit 2023-04-17 17:25 82ea7bc0

View on Github →

feat: port CategoryTheory.Subobject.WellPowered (#3446)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Subobject/WellPowered.lean

added theorem CategoryTheory.essentiallySmall_monoOver_iff_small_subobject

added theorem CategoryTheory.wellPowered_congr

added theorem CategoryTheory.wellPowered_of_equiv

added theorem CategoryTheory.wellPowered_of_essentiallySmall_monoOver