α : Type u_2
β : Type u_1
γ : Type ?u.8654
δ : Type ?u.8657
ι : Type ?u.8660
R : Type ?u.8663
R' : Type ?u.8666
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
s : Set β
f : β → Set α
hs : Set.Countable s
hd : Set.Pairwise s (AEDisjoint μ on f)
h : ∀ (b : β), b ∈ s → NullMeasurableSet (f b)
this : Encodable ↑s
⊢ ↑↑μ (⋃ (b : β) (_ : b ∈ s), f b) = ∑' (p : ↑s), ↑↑μ (f ↑p)
α : Type u_2
β : Type u_1
γ : Type ?u.8654
δ : Type ?u.8657
ι : Type ?u.8660
R : Type ?u.8663
R' : Type ?u.8666
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
s : Set β
f : β → Set α
hs : Set.Countable s
hd : Set.Pairwise s (AEDisjoint μ on f)
h : ∀ (b : β), b ∈ s → NullMeasurableSet (f b)
⊢ ↑↑μ (⋃ (b : β) (_ : b ∈ s), f b) = ∑' (p : ↑s), ↑↑μ (f ↑p)
haveI := hs.toEncodable
α : Type u_2
β : Type u_1
γ : Type ?u.8654
δ : Type ?u.8657
ι : Type ?u.8660
R : Type ?u.8663
R' : Type ?u.8666
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
s : Set β
f : β → Set α
hs : Set.Countable s
hd : Set.Pairwise s (AEDisjoint μ on f)
h : ∀ (b : β), b ∈ s → NullMeasurableSet (f b)
this : Encodable ↑s
⊢ ↑↑μ (⋃ (x : ↑s), f ↑x) = ∑' (p : ↑s), ↑↑μ (f ↑p)
α : Type u_2
β : Type u_1
γ : Type ?u.8654
δ : Type ?u.8657
ι : Type ?u.8660
R : Type ?u.8663
R' : Type ?u.8666
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
s : Set β
f : β → Set α
hs : Set.Countable s
hd : Set.Pairwise s (AEDisjoint μ on f)
h : ∀ (b : β), b ∈ s → NullMeasurableSet (f b)
this : Encodable ↑s
⊢ ↑↑μ (⋃ (b : β) (_ : b ∈ s), f b) = ∑' (p : ↑s), ↑↑μ (f ↑p)
rw [biUnion_eq_iUnion]
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.8654
δ : Type ?u.8657
ι : Type ?u.8660
R : Type ?u.8663
R' : Type ?u.8666
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
s : Set β
f : β → Set α
hs : Set.Countable s
hd : Set.Pairwise s (AEDisjoint μ on f)
h : ∀ (b : β), b ∈ s → NullMeasurableSet (f b)
this : Encodable ↑s
⊢ ↑↑μ (⋃ (x : ↑s), f ↑x) = ∑' (p : ↑s), ↑↑μ (f ↑p)
exact measure_iUnion₀ (hd.on_injective Subtype.coe_injective fun x => x.2) fun x => h x x.2