Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-14 16:19 f6b12763

View on Github →

feat(topology/algebra/infinite_sum): generalize tsum_le_of_sum_range_le (#16951)

Estimated changes

Modified src/topology/algebra/infinite_sum.lean

added theorem tsum_le_of_sum_range_le

Modified src/topology/instances/ennreal.lean

added theorem ennreal.tsum_le_of_sum_range_le

added theorem real.tsum_le_of_sum_range_le

deleted theorem tsum_le_of_sum_range_le