Def CategoryTheory.Functor.essImage.liftFunctor

Modification history

2026-07-31 08:20
Mathlib/CategoryTheory/EssentialImage.lean
chore(CategoryTheory): remove `backward` options using `implicit_reducible` (#42161) …
Modified CategoryTheory.Functor.essImage.liftFunctorView on Github →
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.liftFunctorView on Github →