Commit 2025-03-11 00:25 00d98b7f
View on Github →chore(SetTheory/Cardinal/Cofinality): split file (#21972) The cofinality file is currently a hodgepodge of different results and definitions. We split it as follows:
- Regular and inaccessible cardinals are moved to
SetTheory.Cardinal.Regular
. This file will also be used to define singular cardinals in the near future. - The infinite pigeonhole principle gets its own file. It would've been nice to move ordinal fundamental sequences as well, but they're currently (unnecessarily) used to prove some results on cofinality. A future refactor #19698 will take care of this.