Theorem CategoryTheory.CardinalDirectedPoset.isCardinalPresentable_of_hasCardinalLT_of_le

Modification history

2026-07-03 08:36
Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean
feat(CategoryTheory/Presentable): sharply smaller regular cardinals (#40937) …
Added CategoryTheory.CardinalDirectedPoset.isCardinalPresentable_of_hasCardinalLT_of_leView on Github →