Commit 2024-09-18 06:51 c5befd42

View on Github →

chore(SetTheory/Cardinal/Basic): Cardinal.IsLimit → IsSuccLimit (#16899)

Estimated changes

Modified Mathlib/SetTheory/Cardinal/Basic.lean

added theorem Cardinal.aleph0_le_of_isSuccLimit

added theorem Cardinal.exists_eq_of_iSup_eq_of_not_isSuccLimit

added theorem Cardinal.isSuccLimit_aleph0

added theorem Cardinal.ne_zero_of_isSuccLimit

added theorem Cardinal.not_isSuccLimit_natCast

added theorem Cardinal.not_isSuccLimit_of_lt_aleph0

Modified Mathlib/SetTheory/Cardinal/Cofinality.lean

added theorem Cardinal.IsStrongLimit.aleph0_le

Modified Mathlib/SetTheory/Cardinal/Ordinal.lean

modified theorem Cardinal.add_le_add_iff_of_lt_aleph0