Def CategoryTheory.Functor.essImage.liftFunctorCompIso

Modification history

2025-04-01 10:14
Mathlib/CategoryTheory/EssentialImage.lean
feat: the essential image of a functor is closed under the limits it preserves (#23480) …
Added CategoryTheory.Functor.essImage.liftFunctorCompIsoView on Github →