α✝ : Type ?u.711005
β : Type ?u.711008
γ : Type ?u.711011
δ : Type ?u.711014
ι : Type ?u.711017
R : Type ?u.711020
R' : Type ?u.711023
m0 : MeasurableSpace α✝
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α✝
s✝ s' t : Set α✝
inst✝¹ : NoAtoms μ✝
α : Type u_1
m : MeasurableSpace α
s : Set α
h : Set.Countable s
μ : Measure α
inst✝ : NoAtoms μ
⊢ ↑↑μ (⋃ (x : α) (_ : x ∈ s), {x}) ≤ 0
α✝ : Type ?u.711005
β : Type ?u.711008
γ : Type ?u.711011
δ : Type ?u.711014
ι : Type ?u.711017
R : Type ?u.711020
R' : Type ?u.711023
m0 : MeasurableSpace α✝
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α✝
s✝ s' t : Set α✝
inst✝¹ : NoAtoms μ✝
α : Type u_1
m : MeasurableSpace α
s : Set α
h : Set.Countable s
μ : Measure α
inst✝ : NoAtoms μ
⊢ ↑↑μ s = 0
rw [← biUnion_of_singleton s, ← nonpos_iff_eq_zero]
α✝ : Type ?u.711005
β : Type ?u.711008
γ : Type ?u.711011
δ : Type ?u.711014
ι : Type ?u.711017
R : Type ?u.711020
R' : Type ?u.711023
m0 : MeasurableSpace α✝
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α✝
s✝ s' t : Set α✝
inst✝¹ : NoAtoms μ✝
α : Type u_1
m : MeasurableSpace α
s : Set α
h : Set.Countable s
μ : Measure α
inst✝ : NoAtoms μ
⊢ (∑' (p : ↑s), ↑↑μ {↑p}) ≤ 0
α✝ : Type ?u.711005
β : Type ?u.711008
γ : Type ?u.711011
δ : Type ?u.711014
ι : Type ?u.711017
R : Type ?u.711020
R' : Type ?u.711023
m0 : MeasurableSpace α✝
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α✝
s✝ s' t : Set α✝
inst✝¹ : NoAtoms μ✝
α : Type u_1
m : MeasurableSpace α
s : Set α
h : Set.Countable s
μ : Measure α
inst✝ : NoAtoms μ
⊢ ↑↑μ (⋃ (x : α) (_ : x ∈ s), {x}) ≤ 0
refine' le_trans (measure_biUnion_le h _) _
no goals
α✝ : Type ?u.711005
β : Type ?u.711008
γ : Type ?u.711011
δ : Type ?u.711014
ι : Type ?u.711017
R : Type ?u.711020
R' : Type ?u.711023
m0 : MeasurableSpace α✝
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α✝
s✝ s' t : Set α✝
inst✝¹ : NoAtoms μ✝
α : Type u_1
m : MeasurableSpace α
s : Set α
h : Set.Countable s
μ : Measure α
inst✝ : NoAtoms μ
⊢ (∑' (p : ↑s), ↑↑μ {↑p}) ≤ 0
simp