no goals
α : Type u_2
β : Type u_3
ι : Type ?u.402176
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
s : Set β
hs : MeasurableSet s
inst✝ : Decidable (g a ∈ s)
⊢ (∫ (x : β) in s, f x ∂↑(deterministic g hg) a) = if g a ∈ s then f (g a) else 0
rw [kernel.deterministic_apply, set_integral_dirac' hf _ hs]