no goals
α : Type u_2
β : Type u_3
ι : Type ?u.400065
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : β → E
g : α → β
a : α
hg : Measurable g
hf : StronglyMeasurable f
⊢ (∫ (x : β), f x ∂↑(deterministic g hg) a) = f (g a)
rw [kernel.deterministic_apply, integral_dirac' _ _ hf]