α : Type u_1
β : Type ?u.40097
γ : Type ?u.40100
δ : Type ?u.40103
ι : Type u_2
R : Type ?u.40109
R' : Type ?u.40112
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
s : ι → Set α
hs : ∀ (i : ι), MeasurableSet (s i)
H : Pairwise (Disjoint on s)
⊢ (⨆ (s_1 : Finset ι), ∑ a in s_1, ↑↑μ (s a)) ≤ ↑↑μ univ
α : Type u_1
β : Type ?u.40097
γ : Type ?u.40100
δ : Type ?u.40103
ι : Type u_2
R : Type ?u.40109
R' : Type ?u.40112
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
s : ι → Set α
hs : ∀ (i : ι), MeasurableSet (s i)
H : Pairwise (Disjoint on s)
⊢ (∑' (i : ι), ↑↑μ (s i)) ≤ ↑↑μ univ
rw [ENNReal.tsum_eq_iSup_sum]
no goals
α : Type u_1
β : Type ?u.40097
γ : Type ?u.40100
δ : Type ?u.40103
ι : Type u_2
R : Type ?u.40109
R' : Type ?u.40112
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
s : ι → Set α
hs : ∀ (i : ι), MeasurableSet (s i)
H : Pairwise (Disjoint on s)
⊢ (⨆ (s_1 : Finset ι), ∑ a in s_1, ↑↑μ (s a)) ≤ ↑↑μ univ
exact iSup_le fun s =>
  sum_measure_le_measure_univ (fun i _hi => hs i) fun i _hi j _hj hij => H hij