Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-28 04:03 15b7e536

View on Github →

refactor(set_theory/cardinal/*): cardinal.succ → order.succ (#14273)

Estimated changes

Modified src/data/W/cardinal.lean

Modified src/set_theory/cardinal/basic.lean

deleted theorem cardinal.le_of_lt_succ

deleted theorem cardinal.le_succ

deleted theorem cardinal.lt_succ

deleted theorem cardinal.lt_succ_iff

modified theorem cardinal.powerlt_succ

deleted def cardinal.succ

added theorem cardinal.succ_def

deleted theorem cardinal.succ_le_iff

deleted theorem cardinal.succ_le_of_lt

deleted theorem cardinal.succ_nonempty

modified theorem cardinal.succ_pos

modified theorem cardinal.succ_zero

Modified src/set_theory/cardinal/cofinality.lean

modified theorem cardinal.is_regular_aleph_succ

modified theorem order.cof_le

Modified src/set_theory/cardinal/continuum.lean

Modified src/set_theory/cardinal/ordinal.lean

modified theorem cardinal.aleph'_succ

modified theorem cardinal.aleph_succ

Modified src/set_theory/ordinal/arithmetic.lean

modified theorem ordinal.bmex_lt_ord_succ_card

modified theorem ordinal.mex_lt_ord_succ_mk

Modified src/set_theory/ordinal/basic.lean

modified theorem cardinal.lt_ord_succ_card