Commit 2026-05-21 00:46 c7247814

feat: club sets (#37677) In set theory, a club set is a subset of an ordinal of uncountable cofinality, which is closed in the order topology, and unbounded within the ordinal. We generalize this notion to that of a club set in a well-order α: this is a set which is cofinal and closed under suprema. We recover the more standard notion by setting α = Iio o, whenever ℵ₀ < o.cof. We prove that club sets are closed under intersections of size less than the cofinality of α, and that the fixed points of a normal function are a club set.