Commit 2026-10-21 16:48 cfc1b3da

View on Github →

chore: more filter generalizations in tsum/tprod lemmas (#44511) The new statements are syntactically more general than the old ones.

Estimated changes

Modified Mathlib/MeasureTheory/Function/SimpleFunc.lean

Modified Mathlib/MeasureTheory/Integral/Lebesgue/Basic.lean

Modified Mathlib/MeasureTheory/Integral/Lebesgue/Countable.lean

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

modified theorem Finset.tprod_subtype'

modified theorem Finset.tprod_subtype

modified theorem tprod_singleton