α : Type u_1
β : Type ?u.1693528
γ : Type ?u.1693531
δ : Type ?u.1693534
m : MeasurableSpace α
μ ν : Measure α
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
⊢ (∑' (i : α), ∫⁻ (a : α), f a ∂dirac i) = ∑' (a : α), f a
α : Type u_1
β : Type ?u.1693528
γ : Type ?u.1693531
δ : Type ?u.1693534
m : MeasurableSpace α
μ ν : Measure α
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
⊢ (∫⁻ (a : α), f a ∂count) = ∑' (a : α), f a
rw [count, lintegral_sum_measure]
case e_f
α : Type u_1
β : Type ?u.1693528
γ : Type ?u.1693531
δ : Type ?u.1693534
m : MeasurableSpace α
μ ν : Measure α
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
⊢ (fun i => ∫⁻ (a : α), f a ∂dirac i) = fun a => f a
α : Type u_1
β : Type ?u.1693528
γ : Type ?u.1693531
δ : Type ?u.1693534
m : MeasurableSpace α
μ ν : Measure α
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
⊢ (∑' (i : α), ∫⁻ (a : α), f a ∂dirac i) = ∑' (a : α), f a
congr
no goals
case e_f
α : Type u_1
β : Type ?u.1693528
γ : Type ?u.1693531
δ : Type ?u.1693534
m : MeasurableSpace α
μ ν : Measure α
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
⊢ (fun i => ∫⁻ (a : α), f a ∂dirac i) = fun a => f a
exact funext fun a => lintegral_dirac' a hf