Theorem CategoryTheory.ObjectProperty.IsStrongGenerator.isDense_colimitsCardinalClosure_ι

Modification history

2025-12-05 16:31
Mathlib/CategoryTheory/Presentable/StrongGenerator.lean
feat(CategoryTheory): locally presentable categories and strong generators (#30241) …
Added CategoryTheory.ObjectProperty.IsStrongGenerator.isDense_colimitsCardinalClosure_ιView on Github →