Def CategoryTheory.Functor.RightExtension.isPointwiseRightKanExtensionAtOfIso'

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.RightExtension.isPointwiseRightKanExtensionAtOfIso'View on Github →