Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-28 16:57 e18b9cac

View on Github →

feat(set_theory/continuum): define cardinal.continuum := 2 ^ ω (#9354)

Estimated changes

modified theorem cardinal.mk_Icc_real
modified theorem cardinal.mk_Ici_real
modified theorem cardinal.mk_Ico_real
modified theorem cardinal.mk_Iic_real
modified theorem cardinal.mk_Iio_real
modified theorem cardinal.mk_Ioc_real
modified theorem cardinal.mk_Ioi_real
modified theorem cardinal.mk_Ioo_real
modified theorem cardinal.mk_real
modified theorem cardinal.mk_univ_real
modified theorem cardinal.mk_nat
modified theorem cardinal.nat_cast_inj
modified theorem cardinal.bit0_ne_zero
added theorem cardinal.nat_power_eq
added theorem cardinal.continuum_pos
added theorem cardinal.mk_set_nat