Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-31 18:58 05bd61d0

View on Github →

chore(analysis): move more code out of analysis.normed_space.basic (#10055)

Estimated changes

Created src/analysis/normed/group/completion.lean

added theorem uniform_space.completion.norm_coe

Modified src/analysis/normed/group/hom_completion.lean

Created src/analysis/normed/group/infinite_sum.lean

added theorem cauchy_seq_finset_iff_vanishing_norm

added theorem cauchy_seq_finset_of_norm_bounded

added theorem cauchy_seq_finset_of_summable_norm

added theorem has_sum.norm_le_of_bounded

added theorem has_sum_iff_tendsto_nat_of_summable_norm

added theorem has_sum_of_subseq_of_summable

added theorem nnnorm_tsum_le

added theorem norm_tsum_le_tsum_norm

added theorem summable_iff_vanishing_norm

added theorem summable_of_nnnorm_bounded

added theorem summable_of_norm_bounded

added theorem summable_of_norm_bounded_eventually

added theorem summable_of_summable_nnnorm

added theorem summable_of_summable_norm

added theorem tsum_of_nnnorm_bounded

added theorem tsum_of_norm_bounded

Modified src/analysis/normed_space/basic.lean

deleted theorem cauchy_seq_finset_iff_vanishing_norm

deleted theorem cauchy_seq_finset_of_norm_bounded

deleted theorem cauchy_seq_finset_of_summable_norm

deleted theorem has_sum.norm_le_of_bounded

deleted theorem has_sum_iff_tendsto_nat_of_summable_norm

deleted theorem has_sum_of_subseq_of_summable

deleted theorem nnnorm_tsum_le

deleted theorem norm_tsum_le_tsum_norm

deleted theorem summable_iff_vanishing_norm

deleted theorem summable_of_nnnorm_bounded

deleted theorem summable_of_norm_bounded

deleted theorem summable_of_norm_bounded_eventually

deleted theorem summable_of_summable_nnnorm

deleted theorem summable_of_summable_norm

deleted theorem tsum_of_nnnorm_bounded

deleted theorem tsum_of_norm_bounded

deleted theorem uniform_space.completion.norm_coe

Modified src/topology/uniform_space/completion.lean

modified theorem uniform_space.completion.extension_coe