Theorem CategoryTheory.Functor.hasPointwiseLeftKanExtensionAt_iff_of_equivalence

Modification history

2025-05-27 06:38
Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean
feat(CategoryTheory/Functor): more API for pointwise Kan extensions (#22474) …
Added CategoryTheory.Functor.hasPointwiseLeftKanExtensionAt_iff_of_equivalenceView on Github →