Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-02-12 20:15 a4afa904

View on Github →

refactor(analysis/specific_limits): generalize has_sum_of_absolute_convergence to normed_groups

Estimated changes

Modified src/analysis/normed_space/basic.lean

added theorem norm_triangle_sub

added theorem norm_triangle_sum

Modified src/analysis/specific_limits.lean

added theorem has_sum_iff_cauchy

deleted theorem has_sum_of_absolute_convergence

added theorem has_sum_of_absolute_convergence_real

added theorem has_sum_of_has_sum_norm

deleted theorem is_sum_iff_tendsto_nat_of_nonneg

Modified src/data/finset.lean

added theorem finset.disjoint_sdiff

Modified src/measure_theory/decomposition.lean

Modified src/measure_theory/measure_space.lean

deleted theorem tendsto_at_top_infi_nat

deleted theorem tendsto_at_top_supr_nat

Modified src/order/filter/basic.lean

modified theorem filter.tendsto_at_top_at_top

added theorem filter.tendsto_at_top_principal

Modified src/topology/algebra/topological_structures.lean

added theorem infi_eq_of_tendsto

added theorem tendsto_at_top_infi_nat

added theorem tendsto_at_top_supr_nat

Modified src/topology/instances/ennreal.lean

added theorem ennreal.is_sum_iff_tendsto_nat

modified theorem has_sum_of_nonneg_of_le

added theorem is_sum_iff_tendsto_nat_of_nonneg

modified theorem nnreal.exists_le_is_sum_of_le

added theorem nnreal.is_sum_iff_tendsto_nat

Modified src/topology/metric_space/basic.lean

modified theorem metric.tendsto_at_top

Modified src/topology/uniform_space/basic.lean

added theorem cauchy_iff_exists_le_nhds

added theorem cauchy_map_iff

added theorem cauchy_map_iff_exists_tendsto