Commit 2025-07-12 03:26 67af318f

View on Github →

feat(Topology/ENNReal): Add ENNReal.tsum_biUnion (#18379) This adds infinite versions of Finset.sum_biUnion to ENNReals.

Estimated changes

Modified Mathlib/Data/Set/Lattice.lean

added theorem Set.coe_snd_unionEqSigmaOfDisjoint

added theorem Set.coe_unionEqSigmaOfDisjoint_symm_apply

Modified Mathlib/Data/Set/Pairwise/Lattice.lean

added theorem Set.coe_biUnionEqSigmaOfDisjoint_symm_apply

added theorem Set.coe_snd_biUnionEqSigmaOfDisjoint

Modified Mathlib/Topology/Instances/ENNReal/Lemmas.lean