measure of union of disjoint equal sum

Stream: Is there code for X?

[Pietro Lavino]

I have found m_iUnion to prove this when the sets are pairwise disjoint but in my case I am working with sets whose intersection must be of measure zero.

import Mathlib.Analysis.Convolution
import Mathlib.MeasureTheory.Function.Jacobian
import Mathlib.MeasureTheory.Integral.Bochner
import Mathlib.MeasureTheory.Measure.Lebesgue.Basic
import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Mathlib.Data.ENNReal.Real
import Init.Data.Fin.Basic
import Mathlib.Data.Set.Lattice
import Mathlib.Data.Set.Function
import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Mathlib.Analysis.Convex.Basic
import Mathlib.Data.Real.Basic
import Mathlib.Algebra.BigOperators.Ring

open MeasureTheory
open ENNReal
open Set
open Function
open scoped BigOperators
``````
structure partition {α : Type*} (m : MeasurableSpace α) (μ : Measure α) [IsProbabilityMeasure μ] :=
  f : ℕ → Set α         -- A function from natural numbers to sets of terms in α
  measurable : ∀ n, MeasurableSet (f n)  -- Each set is measurable
  (disjoint : ∀ i j, i ≠ j → μ (f i ∩ f j) = 0)  -- The sets are pairwise disjoint
  (cover : (⋃ n, f n) = Set.univ)  -- The union of all sets covers the entire space
``` and I am trying to prove that ```
theorem addone {α : Type*} {m : MeasurableSpace α} {μ : Measure α} [IsProbabilityMeasure μ]
 (p : partition' m μ) : μ (⋃ i, p.f i) = ∑' i, μ (p.f i) :=
μ.m_iUnion p.measurable p.disjoint

[Rémy Degenne]

I think that you are looking for MeasureTheory.measure_iUnion₀ , which uses a hypothesis with docs#MeasureTheory.AEDisjoint

[Pietro Lavino]

thank you