Theorem CategoryTheory.locallySmall_max

Modification history

2024-05-17 19:31
Mathlib/CategoryTheory/EssentiallySmall.lean
style: remove all isolated `where` (#12991)
Modified CategoryTheory.locallySmall_maxView 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.locallySmall_maxView on Github →