Commit 2025-08-31 01:28 068ec5b9

View on Github →

feat(SetTheory/Cardinal/Aleph): IsStrongLimit (preBeth x) (#26895)

Estimated changes

Modified Mathlib/SetTheory/Cardinal/Aleph.lean

modified theorem Cardinal.isStrongLimit_beth

added theorem Cardinal.isStrongLimit_preBeth

added theorem Cardinal.preBeth_eq_zero

added theorem Cardinal.preBeth_inj

Modified Mathlib/SetTheory/Cardinal/Order.lean

added theorem Cardinal.not_isStrongLimit_zero

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean

added theorem Ordinal.isSuccLimit_add_iff_of_isSuccLimit