Commit 2023-04-18 10:45 f27c11d5

View on Github →

feat: port Data.Real.Cardinality (#3312)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Real/Cardinality.lean

added def Cardinal.cantorFunction

added def Cardinal.cantorFunctionAux

added theorem Cardinal.cantorFunctionAux_eq

added theorem Cardinal.cantorFunctionAux_false

added theorem Cardinal.cantorFunctionAux_nonneg

added theorem Cardinal.cantorFunctionAux_succ

added theorem Cardinal.cantorFunctionAux_true

added theorem Cardinal.cantorFunctionAux_zero

added theorem Cardinal.cantorFunction_injective

added theorem Cardinal.cantorFunction_le

added theorem Cardinal.cantorFunction_succ

added theorem Cardinal.increasing_cantorFunction

added theorem Cardinal.mk_Icc_real

added theorem Cardinal.mk_Ici_real

added theorem Cardinal.mk_Ico_real

added theorem Cardinal.mk_Iic_real

added theorem Cardinal.mk_Iio_real

added theorem Cardinal.mk_Ioc_real

added theorem Cardinal.mk_Ioi_real

added theorem Cardinal.mk_Ioo_real

added theorem Cardinal.mk_real

added theorem Cardinal.mk_univ_real

added theorem Cardinal.not_countable_real

added theorem Cardinal.summable_cantor_function