Theorem CategoryTheory.Functor.hasPointwiseLeftKanExtensionAt_iff_of_natIso

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_natIsoView on Github →