case h
α : Type u_2
β : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → Measure β
hf : Measurable f
a : α
s : Set β
hs : MeasurableSet s
⊢ ↑↑(bind (dirac a) f) s = ↑↑(f a) s
α : Type u_2
β : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → Measure β
hf : Measurable f
a : α
⊢ bind (dirac a) f = f a
ext1 s hs
case h
α : Type u_2
β : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → Measure β
hf : Measurable f
a : α
s : Set β
hs : MeasurableSet s
⊢ ((fun μ => ↑↑μ s) ∘ f) a = ↑↑(f a) s
case h
α : Type u_2
β : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → Measure β
hf : Measurable f
a : α
s : Set β
hs : MeasurableSet s
⊢ ↑↑(bind (dirac a) f) s = ↑↑(f a) s
erw [bind_apply hs hf, lintegral_dirac' a ((measurable_coe hs).comp hf)]
no goals
case h
α : Type u_2
β : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → Measure β
hf : Measurable f
a : α
s : Set β
hs : MeasurableSet s
⊢ ((fun μ => ↑↑μ s) ∘ f) a = ↑↑(f a) s
rfl