Commit 2023-04-09 22:34 f13648cc

View on Github →

feat: port changes to Cardinal files (#3343) My bad for letting these pile up.

Estimated changes

Modified Mathlib/SetTheory/Cardinal/Basic.lean

added theorem Cardinal.IsLimit.aleph0_le

added theorem Cardinal.IsLimit.succ_lt

added def Cardinal.IsLimit

added theorem Cardinal.aleph0_lt_lift

added theorem Cardinal.isLimit_aleph0

added theorem Cardinal.isSuccLimit_aleph0

added theorem Cardinal.isSuccLimit_zero

added theorem Cardinal.lift_le_nat_iff

added theorem Cardinal.lift_lt_aleph0

added theorem Cardinal.lift_lt_nat_iff

added theorem Cardinal.nat_le_lift_iff

added theorem Cardinal.nat_lt_lift_iff

Modified Mathlib/SetTheory/Cardinal/Cofinality.lean

deleted theorem Cardinal.IsLimit.aleph0_le

deleted theorem Cardinal.IsLimit.ne_zero

deleted theorem Cardinal.IsLimit.succ_lt

deleted def Cardinal.IsLimit

deleted theorem Cardinal.isLimit_aleph0

modified theorem Cardinal.isStrongLimit_beth

Modified Mathlib/SetTheory/Cardinal/Continuum.lean

added theorem Cardinal.continuum_le_lift

added theorem Cardinal.continuum_lt_lift

added theorem Cardinal.lift_le_continuum

added theorem Cardinal.lift_lt_continuum

Modified Mathlib/SetTheory/Cardinal/Ordinal.lean

modified theorem Cardinal.aleph'_limit

modified theorem Cardinal.aleph_limit

modified theorem Cardinal.beth_limit

modified theorem Cardinal.ord_aleph_isLimit

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean