α : Type u_2
β : Type u_1
γ : Type ?u.1022236
δ : Type ?u.1022239
m : MeasurableSpace α
μ ν : Measure α
t : Set β
s : β → Set α
ht : Set.Countable t
hm : ∀ (i : β), i ∈ t → NullMeasurableSet (s i)
hd : Set.Pairwise t (AEDisjoint μ on s)
f : α → ℝ≥0∞
this : Encodable ↑t
⊢ (∫⁻ (a : α) in ⋃ (i : β) (_ : i ∈ t), s i, f a ∂μ) = ∑' (i : ↑t), ∫⁻ (a : α) in s ↑i, f a ∂μ
α : Type u_2
β : Type u_1
γ : Type ?u.1022236
δ : Type ?u.1022239
m : MeasurableSpace α
μ ν : Measure α
t : Set β
s : β → Set α
ht : Set.Countable t
hm : ∀ (i : β), i ∈ t → NullMeasurableSet (s i)
hd : Set.Pairwise t (AEDisjoint μ on s)
f : α → ℝ≥0∞
⊢ (∫⁻ (a : α) in ⋃ (i : β) (_ : i ∈ t), s i, f a ∂μ) = ∑' (i : ↑t), ∫⁻ (a : α) in s ↑i, f a ∂μ
haveI := ht.toEncodable
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.1022236
δ : Type ?u.1022239
m : MeasurableSpace α
μ ν : Measure α
t : Set β
s : β → Set α
ht : Set.Countable t
hm : ∀ (i : β), i ∈ t → NullMeasurableSet (s i)
hd : Set.Pairwise t (AEDisjoint μ on s)
f : α → ℝ≥0∞
this : Encodable ↑t
⊢ (∫⁻ (a : α) in ⋃ (i : β) (_ : i ∈ t), s i, f a ∂μ) = ∑' (i : ↑t), ∫⁻ (a : α) in s ↑i, f a ∂μ
rw [biUnion_eq_iUnion, lintegral_iUnion₀ (SetCoe.forall'.1 hm) (hd.subtype _ _)]