Theorem CategoryTheory.Functor.DenseAt.hasPointwiseLeftKanExtensionAt

Modification history

2026-05-26 05:31
Mathlib/CategoryTheory/Functor/KanExtension/DenseAt.lean
chore(CategoryTheory/Functor): more API for dense functors (#39845) …
Added CategoryTheory.Functor.DenseAt.hasPointwiseLeftKanExtensionAtView on Github →