Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-02-13 17:01 3fd0e60a

View on Github →

refactor(topology/algebra/infinite_sum): Cauchy condition for infinite sums generalized to complete topological groups

Estimated changes

added theorem ball_0_eq
added theorem norm_tsum_le_tsum_norm
deleted theorem has_sum_iff_cauchy
deleted theorem has_sum_of_has_sum_norm
modified def pmf.pure
added theorem filter.tendsto_at_top'
modified theorem filter.tendsto_at_top
added theorem has_sum_iff_cauchy
added theorem has_sum_iff_vanishing
modified theorem has_sum_of_has_sum_of_sub
deleted theorem is_sum_ite
added theorem is_sum_ite_eq
added theorem is_sum_le_inj
added def option.cases_on'
deleted theorem tsum_ite
added theorem tsum_ite_eq
added theorem exists_nhds_split_inv