Def CategoryTheory.Functor.LeftExtension.isPointwiseLeftKanExtensionAtOfIso'

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.LeftExtension.isPointwiseLeftKanExtensionAtOfIso'View on Github →