Commit 2023-02-24 08:05 43fabded

View on Github →

feat: Port SetTheory.Cardinal.Continuum (#2474)

Estimated changes

Modified Mathlib.lean

Created Mathlib/SetTheory/Cardinal/Continuum.lean

added theorem Cardinal.aleph0_add_continuum

added theorem Cardinal.aleph0_le_continuum

added theorem Cardinal.aleph0_lt_continuum

added theorem Cardinal.aleph0_mul_continuum

added theorem Cardinal.aleph0_power_aleph0

added theorem Cardinal.aleph_one_le_continuum

added theorem Cardinal.beth_one

added def Cardinal.continuum

added theorem Cardinal.continuum_add_aleph0

added theorem Cardinal.continuum_add_nat

added theorem Cardinal.continuum_add_self

added theorem Cardinal.continuum_mul_aleph0

added theorem Cardinal.continuum_mul_nat

added theorem Cardinal.continuum_mul_self

added theorem Cardinal.continuum_ne_zero

added theorem Cardinal.continuum_pos

added theorem Cardinal.continuum_power_aleph0

added theorem Cardinal.continuum_toNat

added theorem Cardinal.continuum_toPartENat

added theorem Cardinal.lift_continuum

added theorem Cardinal.mk_set_nat

added theorem Cardinal.nat_add_continuum

added theorem Cardinal.nat_lt_continuum

added theorem Cardinal.nat_mul_continuum

added theorem Cardinal.nat_power_aleph0

added theorem Cardinal.two_power_aleph0