α : Type u_2
β : Type u_1
γ : Type ?u.17750
δ : Type ?u.17753
ι : Type ?u.17756
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
s : Finset β
f : β → Set α
⊢ ↑↑μ (⋃ (b : β) (_ : b ∈ s), f b) ≤ ∑' (b : { x // x ∈ s }), ↑↑μ (f ↑b)
α : Type u_2
β : Type u_1
γ : Type ?u.17750
δ : Type ?u.17753
ι : Type ?u.17756
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
s : Finset β
f : β → Set α
⊢ ↑↑μ (⋃ (b : β) (_ : b ∈ s), f b) ≤ ∑ p in s, ↑↑μ (f p)
rw [← Finset.sum_attach, Finset.attach_eq_univ, ← tsum_fintype]
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.17750
δ : Type ?u.17753
ι : Type ?u.17756
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
s : Finset β
f : β → Set α
⊢ ↑↑μ (⋃ (b : β) (_ : b ∈ s), f b) ≤ ∑' (b : { x // x ∈ s }), ↑↑μ (f ↑b)
exact measure_biUnion_le s.countable_toSet f