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.

Estimated changes

deleted theorem Cardinal.IsRegular.cof_eq
deleted theorem Cardinal.IsRegular.nat_lt
deleted theorem Cardinal.IsRegular.pos
deleted def Cardinal.IsRegular
deleted theorem Cardinal.deriv_lt_ord
deleted theorem Cardinal.isRegular_aleph0
deleted theorem Cardinal.isRegular_cof
deleted theorem Cardinal.isRegular_succ
modified theorem Cardinal.lt_cof_power
modified theorem Cardinal.lt_power_cof
added theorem Cardinal.IsRegular.pos
added theorem Cardinal.deriv_lt_ord
added theorem Cardinal.isRegular_cof