Commit 2026-04-18 06:23 dfae8cda

View on Github →

chore(SetTheory/Cardinal): tweak succ lemmas (#36965) We leave the SuccOrder instance unexposed. It doesn't have any particularly good def-eqs, it's simply defined as the infimum of all larger cardinals. We also golf some surrounding theorems.

Estimated changes

Modified Mathlib/LinearAlgebra/Dimension/Basic.lean

Modified Mathlib/Order/SuccPred/CompleteLinearOrder.lean

Modified Mathlib/SetTheory/Cardinal/Basic.lean

added theorem Cardinal.lt_natCast_add_one_iff

Modified Mathlib/SetTheory/Cardinal/Order.lean

added theorem Cardinal.add_one_le_of_lt

modified theorem Cardinal.add_one_le_succ

modified theorem Cardinal.lift_succ

Modified Mathlib/SetTheory/Ordinal/Basic.lean