Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-07-02 11:28 b4989a04

View on Github →

compute the cardinality of real (#1096)

compute the cardinality of real
minor improvements
fix(data/rat/denumerable): change namespace of of_rat
style(src/topology/algebra/infinite_sum): structure proof

Estimated changes

Modified src/data/equiv/denumerable.lean

Modified src/data/equiv/nat.lean

added def equiv.pnat_equiv_nat

Modified src/data/fintype.lean

added theorem not_nonempty_fintype

Modified src/data/rat/denumerable.lean

added theorem cardinal.mk_rat

Created src/data/real/cardinality.lean

added def cardinal.cantor_function

added def cardinal.cantor_function_aux

added theorem cardinal.cantor_function_aux_eq

added theorem cardinal.cantor_function_aux_ff

added theorem cardinal.cantor_function_aux_nonneg

added theorem cardinal.cantor_function_aux_succ

added theorem cardinal.cantor_function_aux_tt

added theorem cardinal.cantor_function_le

added theorem cardinal.cantor_function_succ

added theorem cardinal.increasing_cantor_function

added theorem cardinal.injective_cantor_function

added theorem cardinal.mk_real

added theorem cardinal.not_countable_real

added theorem cardinal.summable_cantor_function

Modified src/set_theory/cardinal.lean

added theorem cardinal.denumerable_iff

added theorem cardinal.infinite_iff

added theorem cardinal.mk_int

added theorem cardinal.mk_nat

added theorem cardinal.mk_pnat

modified theorem cardinal.mul_def

Modified src/set_theory/ordinal.lean

added theorem cardinal.power_self_eq

Modified src/topology/algebra/infinite_sum.lean

added theorem tsum_eq_zero_add