Commit 2021-11-23 13:11 3b137447
View on Github →chore(measure_theory/integral): more versions of integral_finset_sum
(#10394)
- fix assumptions in existing lemmas (
∀ i ∈ s
instead of∀ i
); - add a version for interval integrals.
chore(measure_theory/integral): more versions of integral_finset_sum
(#10394)
∀ i ∈ s
instead of ∀ i
);