α : Type u_1
β : Type u_2
γ : Type ?u.807482
δ : Type ?u.807485
inst✝¹ : MeasurableSpace α
K : Type ?u.807491
inst✝ : Zero β
f : α →ₛ β
s : Set α
hs : MeasurableSet s
⊢ ↑(piecewise s hs f 0) = indicator s ↑f
α : Type u_1
β : Type u_2
γ : Type ?u.807482
δ : Type ?u.807485
inst✝¹ : MeasurableSpace α
K : Type ?u.807491
inst✝ : Zero β
f : α →ₛ β
s : Set α
hs : MeasurableSet s
⊢ ↑(restrict f s) = indicator s ↑f
rw [restrict, dif_pos hs]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.807482
δ : Type ?u.807485
inst✝¹ : MeasurableSpace α
K : Type ?u.807491
inst✝ : Zero β
f : α →ₛ β
s : Set α
hs : MeasurableSet s
⊢ ↑(piecewise s hs f 0) = indicator s ↑f
rfl