α : Type u_1
β : Type ?u.3729
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
hs : MeasurableSet s
⊢ Measurable fun b => ↑↑(dirac b) s
α : Type u_1
β : Type ?u.3729
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
⊢ Measurable dirac
refine' measurable_of_measurable_coe _ fun s hs => _
α : Type u_1
β : Type ?u.3729
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
hs : MeasurableSet s
⊢ Measurable fun b => indicator s 1 b
α : Type u_1
β : Type ?u.3729
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
hs : MeasurableSet s
⊢ Measurable fun b => ↑↑(dirac b) s
simp_rw [dirac_apply' _ hs]
no goals
α : Type u_1
β : Type ?u.3729
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
hs : MeasurableSet s
⊢ Measurable fun b => indicator s 1 b
exact measurable_one.indicator hs