Def CategoryTheory.CardinalFilteredPoset.PropSet

Modification history

2026-07-03 08:36

Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean

feat(CategoryTheory/Presentable): sharply smaller regular cardinals (#40937) …

Deleted CategoryTheory.CardinalFilteredPoset.PropSet View on Github →

2026-06-18 10:58

Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean

feat(CategoryTheory): the κ-accessible category of κ-directed posets (#39655) …

Added CategoryTheory.CardinalFilteredPoset.PropSet View on Github →