Theorem CategoryTheory.essentiallySmall_of_small_of_locallySmall

Modification history

2025-10-28 20:32
Mathlib/CategoryTheory/EssentiallySmall.lean
chore(CategoryTheory/EssentiallySmall): adding an instance (#30534) …
Deleted CategoryTheory.essentiallySmall_of_small_of_locallySmallView on Github →
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_locallySmallView on Github →