Commit 2023-03-06 08:57 934223d3

View on Github →

feat: port Topology.Algebra.InfiniteSum.Order (#2644)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Topology/Algebra/InfiniteSum/Basic.lean

added theorem hasSum_extend_zero

added theorem summable_extend_zero

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

added theorem Finite.of_summable_const

added theorem HasSum.nonneg

added theorem HasSum.nonpos

added theorem Set.Finite.of_summable_const

added theorem Summable.tendsto_atTop_of_pos

added theorem hasSum_le

added theorem hasSum_le_inj

added theorem hasSum_le_of_sum_le

added theorem hasSum_lt

added theorem hasSum_mono

added theorem hasSum_of_isLUB

added theorem hasSum_of_isLUB_of_nonneg

added theorem hasSum_strict_mono

added theorem hasSum_zero_iff

added theorem hasSum_zero_iff_of_nonneg

added theorem isLUB_hasSum

added theorem isLUB_has_sum'

added theorem le_hasSum

added theorem le_hasSum_of_le_sum

added theorem le_has_sum'

added theorem le_tsum'

added theorem le_tsum

added theorem sum_le_hasSum

added theorem sum_le_tsum

added theorem summable_abs_iff

added theorem tsum_eq_zero_iff

added theorem tsum_le_of_sum_le'

added theorem tsum_le_of_sum_le

added theorem tsum_le_of_sum_range_le

added theorem tsum_le_tsum

added theorem tsum_le_tsum_of_inj

added theorem tsum_lt_tsum

added theorem tsum_mono

added theorem tsum_ne_zero_iff

added theorem tsum_nonneg

added theorem tsum_nonpos

added theorem tsum_pos

added theorem tsum_strict_mono