Commit 2024-07-04 14:02 202e9e09
View on Github →feat: dualising results in CategoryTheory.Functor.KanExtension.Pointwise (#14258)
In this PR, we make a left/right synchronization of the API in the file CategoryTheory.Functor.KanExtension.Pointwise: missing definitions/lemmas for pointwise right Kan extensions are introduced.
Estimated changes
added theorem CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtension.hasPointwiseRightKanExtension
added theorem CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtension.hasRightKanExtension
added theorem CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtension.isRightKanExtension