Theorem CategoryTheory.yonedaYonedaColimit_app_inv

Modification history

2024-10-20 16:57
Mathlib/CategoryTheory/Limits/Preserves/Yoneda.lean
feat(CategoryTheory): pull colimits out of hom functors with Yoneda on the LHS (#17440) …
Added CategoryTheory.yonedaYonedaColimit_app_invView on Github →