α : Type u_2
β : Type ?u.39043
γ : Type ?u.39046
δ : Type ?u.39049
ι : Type u_1
R : Type ?u.39055
R' : Type ?u.39058
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t✝ : Set α
s : Finset ι
t : ι → Set α
h : ∀ (i : ι), i ∈ s → MeasurableSet (t i)
H : PairwiseDisjoint (↑s) t
⊢ ↑↑μ (⋃ (b : ι) (_ : b ∈ s), t b) ≤ ↑↑μ univ
α : Type u_2
β : Type ?u.39043
γ : Type ?u.39046
δ : Type ?u.39049
ι : Type u_1
R : Type ?u.39055
R' : Type ?u.39058
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t✝ : Set α
s : Finset ι
t : ι → Set α
h : ∀ (i : ι), i ∈ s → MeasurableSet (t i)
H : PairwiseDisjoint (↑s) t
⊢ ∑ i in s, ↑↑μ (t i) ≤ ↑↑μ univ
rw [← measure_biUnion_finset H h]
no goals
α : Type u_2
β : Type ?u.39043
γ : Type ?u.39046
δ : Type ?u.39049
ι : Type u_1
R : Type ?u.39055
R' : Type ?u.39058
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t✝ : Set α
s : Finset ι
t : ι → Set α
h : ∀ (i : ι), i ∈ s → MeasurableSet (t i)
H : PairwiseDisjoint (↑s) t
⊢ ↑↑μ (⋃ (b : ι) (_ : b ∈ s), t b) ≤ ↑↑μ univ
exact measure_mono (subset_univ _)