α : Type u_2
m0 : MeasurableSpace α
μ✝ μ₁ μ₂ ν ν₁ ν₂ : Measure α
ι : Type u_1
inst✝ : Countable ι
μ : ι → Measure α
H : ∀ (i : ι), μ i ⟂ₘ ν
⊢ sum μ ⟂ₘ ν
α : Type u_2
m0 : MeasurableSpace α
μ✝ μ₁ μ₂ ν ν₁ ν₂ : Measure α
ι : Type u_1
inst✝ : Countable ι
μ : ι → Measure α
⊢ sum μ ⟂ₘ ν ↔ ∀ (i : ι), μ i ⟂ₘ ν
refine' ⟨fun h i => h.mono (le_sum _ _) le_rfl, fun H => _⟩
α : Type u_2
m0 : MeasurableSpace α
μ✝ μ₁ μ₂ ν ν₁ ν₂ : Measure α
ι : Type u_1
inst✝ : Countable ι
μ : ι → Measure α
s : ι → Set α
hsm : ∀ (i : ι), MeasurableSet (s i)
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsν : ∀ (i : ι), ↑↑ν (s iᶜ) = 0
⊢ sum μ ⟂ₘ ν
α : Type u_2
m0 : MeasurableSpace α
μ✝ μ₁ μ₂ ν ν₁ ν₂ : Measure α
ι : Type u_1
inst✝ : Countable ι
μ : ι → Measure α
H : ∀ (i : ι), μ i ⟂ₘ ν
⊢ sum μ ⟂ₘ ν
choose s hsm hsμ hsν using H
case refine'_1
α : Type u_2
m0 : MeasurableSpace α
μ✝ μ₁ μ₂ ν ν₁ ν₂ : Measure α
ι : Type u_1
inst✝ : Countable ι
μ : ι → Measure α
s : ι → Set α
hsm : ∀ (i : ι), MeasurableSet (s i)
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsν : ∀ (i : ι), ↑↑ν (s iᶜ) = 0
⊢ ↑↑(sum μ) (⋂ (i : ι), s i) = 0

case refine'_2
α : Type u_2
m0 : MeasurableSpace α
μ✝ μ₁ μ₂ ν ν₁ ν₂ : Measure α
ι : Type u_1
inst✝ : Countable ι
μ : ι → Measure α
s : ι → Set α
hsm : ∀ (i : ι), MeasurableSet (s i)
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsν : ∀ (i : ι), ↑↑ν (s iᶜ) = 0
⊢ ↑↑ν ((⋂ (i : ι), s i)ᶜ) = 0
α : Type u_2
m0 : MeasurableSpace α
μ✝ μ₁ μ₂ ν ν₁ ν₂ : Measure α
ι : Type u_1
inst✝ : Countable ι
μ : ι → Measure α
s : ι → Set α
hsm : ∀ (i : ι), MeasurableSet (s i)
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsν : ∀ (i : ι), ↑↑ν (s iᶜ) = 0
⊢ sum μ ⟂ₘ ν
refine' ⟨⋂ i, s i, MeasurableSet.iInter hsm, _, _⟩
case refine'_1
α : Type u_2
m0 : MeasurableSpace α
μ✝ μ₁ μ₂ ν ν₁ ν₂ : Measure α
ι : Type u_1
inst✝ : Countable ι
μ : ι → Measure α
s : ι → Set α
hsm : ∀ (i : ι), MeasurableSet (s i)
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsν : ∀ (i : ι), ↑↑ν (s iᶜ) = 0
⊢ ∀ (i : ι), ↑↑(μ i) (⋂ (b : ι), s b) = 0
case refine'_1
α : Type u_2
m0 : MeasurableSpace α
μ✝ μ₁ μ₂ ν ν₁ ν₂ : Measure α
ι : Type u_1
inst✝ : Countable ι
μ : ι → Measure α
s : ι → Set α
hsm : ∀ (i : ι), MeasurableSet (s i)
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsν : ∀ (i : ι), ↑↑ν (s iᶜ) = 0
⊢ ↑↑(sum μ) (⋂ (i : ι), s i) = 0
rw [sum_apply _ (MeasurableSet.iInter hsm), ENNReal.tsum_eq_zero]
no goals
case refine'_1
α : Type u_2
m0 : MeasurableSpace α
μ✝ μ₁ μ₂ ν ν₁ ν₂ : Measure α
ι : Type u_1
inst✝ : Countable ι
μ : ι → Measure α
s : ι → Set α
hsm : ∀ (i : ι), MeasurableSet (s i)
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsν : ∀ (i : ι), ↑↑ν (s iᶜ) = 0
⊢ ∀ (i : ι), ↑↑(μ i) (⋂ (b : ι), s b) = 0
exact fun i => measure_mono_null (iInter_subset _ _) (hsμ i)
no goals
case refine'_2
α : Type u_2
m0 : MeasurableSpace α
μ✝ μ₁ μ₂ ν ν₁ ν₂ : Measure α
ι : Type u_1
inst✝ : Countable ι
μ : ι → Measure α
s : ι → Set α
hsm : ∀ (i : ι), MeasurableSet (s i)
hsμ : ∀ (i : ι), ↑↑(μ i) (s i) = 0
hsν : ∀ (i : ι), ↑↑ν (s iᶜ) = 0
⊢ ↑↑ν ((⋂ (i : ι), s i)ᶜ) = 0
rwa [compl_iInter, measure_iUnion_null_iff]