Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-09-20 18:29 46988284

View on Github →

feat(topology): prove geometric series

Estimated changes

Modified algebra/big_operators.lean

added theorem finset.abs_sum_le_sum_abs

added theorem finset.prod_sdiff

Modified algebra/group_power.lean

added theorem inv_inv'

added theorem inv_one

modified theorem pow_ge_one_of_ge_one

added theorem pow_inv

added theorem pow_le_pow

added theorem pow_ne_zero

added theorem pow_nonneg

modified theorem pow_pos

modified theorem pow_succ'

Modified data/finset/basic.lean

added theorem finset.exists_nat_subset_upto

added theorem finset.not_mem_upto

added theorem finset.sdiff_subset_sdiff

added theorem finset.upto_subset_upto_iff

Modified topology/infinite_sum.lean

added theorem add_div

added theorem filter.mem_at_top

added theorem has_sum_of_absolute_convergence

added theorem is_sum_iff_tendsto_nat_of_nonneg

added theorem tendsto_sum_nat_of_is_sum

Created topology/limits.lean

added theorem div_eq_mul_inv

added theorem exists_lt_of_nat

added theorem int_of_nat_eq_of_nat

added theorem inv_pos

added theorem is_sum_geometric

added theorem map_succ_at_top_eq

added theorem mul_add_one_le_pow

added theorem neg_inv

added def of_nat

added theorem of_nat_add

added theorem of_nat_bit0

added theorem of_nat_bit1

added theorem of_nat_le_of_nat

added theorem of_nat_le_of_nat_iff

added theorem of_nat_mul

added theorem of_nat_one

added theorem of_nat_sub

added theorem one_lt_inv

added theorem rat_coe_eq_of_nat

added theorem rat_of_nat_eq_of_nat

added theorem real_of_rat_of_nat_eq_of_nat

added theorem sum_geometric'

added theorem sum_geometric

added theorem tendsto_comp_succ_at_top_iff

added theorem tendsto_inverse_at_top_nhds_0

added theorem tendsto_pow_at_top_at_top_of_gt_1

added theorem tendsto_pow_at_top_nhds_0_of_lt_1

added theorem zero_le_of_nat

Modified topology/metric_space.lean

added theorem mem_uniformity_dist

Modified topology/real.lean