Def CategoryTheory.CardinalFilteredPoset.hasCardinalLTWithTerminal

Modification history

2026-07-03 08:36
Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean
feat(CategoryTheory/Presentable): sharply smaller regular cardinals (#40937) …
Deleted CategoryTheory.CardinalFilteredPoset.hasCardinalLTWithTerminalView on Github →
2026-06-18 10:58
Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean
feat(CategoryTheory): the κ-accessible category of κ-directed posets (#39655) …
Added CategoryTheory.CardinalFilteredPoset.hasCardinalLTWithTerminalView on Github →