Theorem CategoryTheory.Functor.isDense_iff_nonempty_isPointwiseLeftKanExtension

Modification history

2025-11-17 00:03
Mathlib/CategoryTheory/Functor/KanExtension/Dense.lean
feat(CategoryTheory): dense functors (#29565) …
Added CategoryTheory.Functor.isDense_iff_nonempty_isPointwiseLeftKanExtensionView on Github →