no goals
α : Type u_1
β : Type ?u.1730339
γ : Type ?u.1730342
δ : Type ?u.1730345
m : MeasurableSpace α
μ ν : Measure α
inst✝ : MeasurableSingletonClass α
f : α → ℝ≥0∞
s : Set α
hs : Set.Countable s
⊢ (∫⁻ (a : α) in s, f a ∂μ) = ∫⁻ (a : α) in ⋃ (x : α) (_ : x ∈ s), {x}, f a ∂μ
rw [biUnion_of_singleton]
no goals
α : Type u_1
β : Type ?u.1730339
γ : Type ?u.1730342
δ : Type ?u.1730345
m : MeasurableSpace α
μ ν : Measure α
inst✝ : MeasurableSingletonClass α
f : α → ℝ≥0∞
s : Set α
hs : Set.Countable s
⊢ (∑' (a : ↑s), ∫⁻ (x : α) in {↑a}, f x ∂μ) = ∑' (a : ↑s), f ↑a * ↑↑μ {↑a}
simp only [lintegral_singleton]