Theorem CategoryTheory.Functor.isDense_iff_fullyFaithful_restrictedULiftYoneda

Modification history

2026-10-31 10:05
Mathlib/CategoryTheory/Functor/KanExtension/Dense.lean
refactor(CategoryTheory): colimits of representable presheaves (#42816) …
Modified CategoryTheory.Functor.isDense_iff_fullyFaithful_restrictedULiftYonedaView on Github →
2025-11-17 00:03
Mathlib/CategoryTheory/Functor/KanExtension/Dense.lean
feat(CategoryTheory): dense functors (#29565) …
Added CategoryTheory.Functor.isDense_iff_fullyFaithful_restrictedULiftYonedaView on Github →