no goals
α : Type u_1
β : Type u_2
ι : Type ?u.398685
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
f : β → ℝ≥0∞
g : α → β
a : α
hg : Measurable g
hf : Measurable 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_lintegral_dirac' hf hs]