Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes