Commit 2026-07-03 08:36 4d076302

feat(CategoryTheory/Presentable): sharply smaller regular cardinals (#40937) In this file, we introduce the predicate Cardinal.SharplyLT. Given two regular cardinals κ₁ < κ₂, this condition can be described in different ways (a TFAE lemma will appear in a future PR). Here, we define it by saying that the category CardinalDirectedPoset κ₁ is κ₂-accessible, and we show one of the implications for the future TFAE lemma. (This PR also renames CardinalFilteredPoset as CardinalDirectedPoset.)