Commit 2026-10-20 00:10 4dc3912c

View on Github →

feat(Topology/Algebra/InfiniteSum): Generalize ENNReal lemmas (#38489) This PR generalizes many theorems in Topology/Algebra/InfiniteSum/ENNReal.lean from ENNREal to any type that satisfies a list of order-related instances, mostly [CommMonoid α] [CompleteLattice α] [CanonicallyOrderedMul α] [TopologicalSpace α] [SupConvergenceClass α] Deprecation of the original ENNReal lemmas are done in the next PR: #38193. Related Zulip thread: #Is there code for X? > Summing ENats without topology

Estimated changes

added theorem CompleteLattice.hasSum
added theorem le_tsum
added theorem le_tsum_of_mem
added theorem mul_tsum
added theorem ne_top_of_tsum_ne_top
added theorem singleton_add_tsum_ne
added theorem sum_add_tsum_compl
added theorem sum_le_tsum
added theorem tsum_add
added theorem tsum_biUnion
added theorem tsum_biUnion_le
added theorem tsum_biUnion_le_tsum
added theorem tsum_comm
added theorem tsum_eq_add_tsum_ite
added theorem tsum_eq_iSup_sum'
added theorem tsum_eq_iSup_sum
added theorem tsum_eq_top_of_eq_top
added theorem tsum_eq_zero_iff
added theorem tsum_fiberwise
added theorem tsum_iUnion
added theorem tsum_iUnion_eq_tsum
added theorem tsum_iUnion_le
added theorem tsum_iUnion_le_sum
added theorem tsum_iUnion_le_tsum
added theorem tsum_insert
added theorem tsum_le_of_subset
added theorem tsum_le_tsum
added theorem tsum_mono_subtype
added theorem tsum_mul
added theorem tsum_prod'
added theorem tsum_prod
added theorem tsum_sigma'
added theorem tsum_sigma
added theorem tsum_top
added theorem tsum_union_le
added theorem tsum_union_of_disjoint