Theorem CategoryTheory.Functor.ranObjObjIsoLimit_inv_π

Modification history

2024-10-19 19:08
Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean
feat(CategoryTheory/KanExtensions): Evaluating `lan` twice amounts to taking a colimit (#17531)
Added CategoryTheory.Functor.ranObjObjIsoLimit_inv_πView on Github →