Mathlib Changelog
v4
Changelog
About
Github
Theorem
CategoryTheory.essentiallySmall_of_small_of_locallySmall
Modification history
2023-09-08 11:01
Mathlib/CategoryTheory/EssentiallySmall.lean
feat: a functor from a small category to a filtered category factors through a small filtered category (#6212)
Added
CategoryTheory.essentiallySmall_of_small_of_locallySmall
View on Github →