Commit 2023-02-23 08:11 7592384a

View on Github →

feat: Port CategoryTheory.EssentiallySmall (#2452)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/EssentiallySmall.lean

added theorem CategoryTheory.Discrete.essentiallySmallOfSmall

added theorem CategoryTheory.EssentiallySmall.mk'

added def CategoryTheory.ShrinkHoms.fromShrinkHoms

added theorem CategoryTheory.ShrinkHoms.from_to

added def CategoryTheory.ShrinkHoms.toShrinkHoms

added theorem CategoryTheory.ShrinkHoms.to_from

added def CategoryTheory.ShrinkHoms

added def CategoryTheory.SmallModel

added theorem CategoryTheory.essentiallySmallSelf

added theorem CategoryTheory.essentiallySmall_congr

added theorem CategoryTheory.essentiallySmall_iff

added theorem CategoryTheory.essentiallySmall_iff_of_thin

added theorem CategoryTheory.locallySmall_congr