Commit 2023-03-07 06:34 331d9ef0

View on Github →

feat: port Topology.Algebra.InfiniteSum.Real (#2673)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Algebra/InfiniteSum/Real.lean

added theorem cauchySeq_of_dist_le_of_summable

added theorem cauchySeq_of_edist_le_of_summable

added theorem cauchySeq_of_summable_dist

added theorem dist_le_tsum_dist_of_tendsto

added theorem dist_le_tsum_dist_of_tendsto₀

added theorem dist_le_tsum_of_dist_le_of_tendsto

added theorem dist_le_tsum_of_dist_le_of_tendsto₀