α : Type u_1
β : Type ?u.7470
γ : Type ?u.7473
a a' : α
s✝ : Set α
inst✝ : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ (if a ∈ s then 1 else 0) = Set.indicator s 1 a
α : Type u_1
β : Type ?u.7470
γ : Type ?u.7473
a a' : α
s✝ : Set α
inst✝ : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ ↑↑(toMeasure (pure a)) s = ↑↑(Measure.dirac a) s
rw [toMeasure_pure_apply a s hs, Measure.dirac_apply' a hs]
no goals
α : Type u_1
β : Type ?u.7470
γ : Type ?u.7473
a a' : α
s✝ : Set α
inst✝ : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ (if a ∈ s then 1 else 0) = Set.indicator s 1 a
rfl