Commit 2026-10-17 10:55 1bcf70fe

View on Github →

chore(SetTheory/Cardinal/Aleph): fix some theorem names (#44859) The preferred form for succ x over the ordinals is x + 1.

Estimated changes

Modified Mathlib/SetTheory/Cardinal/Aleph.lean

deleted theorem Cardinal.preBeth_nat

added theorem Cardinal.preBeth_natCast

added theorem Ordinal.isInitial_add_one

Modified Mathlib/SetTheory/Cardinal/Continuum.lean

modified theorem Cardinal.beth_one