Theorem CategoryTheory.ObjectProperty.colimitsCardinalClosure_le_isCardinalPresentable

Modification history

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