α : Type u_1
β : Type u_2
ι : Type ?u.395518
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
f : α → β
hf : Measurable f
a : α
s : Set β
hs : MeasurableSet s
⊢ ↑↑(↑{ val := fun a => Measure.dirac (f a), property := (_ : Measurable fun a => Measure.dirac (f a)) } a) s =
    Set.indicator s (fun x => 1) (f a)
α : Type u_1
β : Type u_2
ι : Type ?u.395518
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
f : α → β
hf : Measurable f
a : α
s : Set β
hs : MeasurableSet s
⊢ ↑↑(↑(deterministic f hf) a) s = Set.indicator s (fun x => 1) (f a)
rw [deterministic]
α : Type u_1
β : Type u_2
ι : Type ?u.395518
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
f : α → β
hf : Measurable f
a : α
s : Set β
hs : MeasurableSet s
⊢ ↑↑(Measure.dirac (f a)) s = Set.indicator s 1 (f a)
α : Type u_1
β : Type u_2
ι : Type ?u.395518
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
f : α → β
hf : Measurable f
a : α
s : Set β
hs : MeasurableSet s
⊢ ↑↑(↑{ val := fun a => Measure.dirac (f a), property := (_ : Measurable fun a => Measure.dirac (f a)) } a) s =
    Set.indicator s (fun x => 1) (f a)
change Measure.dirac (f a) s = s.indicator 1 (f a)
no goals
α : Type u_1
β : Type u_2
ι : Type ?u.395518
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : { x // x ∈ kernel α β }
f : α → β
hf : Measurable f
a : α
s : Set β
hs : MeasurableSet s
⊢ ↑↑(Measure.dirac (f a)) s = Set.indicator s 1 (f a)
simp_rw [Measure.dirac_apply' _ hs]