Commit 2026-03-27 17:02 a58cf2dc

View on Github →

feat: countable limit ordinal has cofinality ℵ₀ (#37029)

Estimated changes

added theorem Order.cof_eq_aleph0
added theorem Order.cof_int
added theorem Order.cof_nat
modified theorem Ordinal.cof_omega0