Commit 2025-03-04 18:52 a3eb5448

feat(SetTheory/Cardinal/Aleph): introduce pre-beth function (#20749) We introduce the "pre-beth" function, recursively defined by preBeth o = ⨆ a : Iio o, 2 ^ preBeth a. This is like the same as the usual beth function, but starting at 0 rather than ℵ₀. This function is relevant in the context of the von Neumann hierarchy, which satisfies #(V_ o) = preBeth o. We also simplify proofs about the standard beth function, by proving them in terms of this auxiliary function.