α : Type u_1
β : Type u_2
γ : Type ?u.42149
δ : Type ?u.42152
inst✝ : MeasurableSpace α
f g : α →ₛ β
⊢ Set.piecewise ∅ ↑f ↑g = ↑g
α : Type u_1
β : Type u_2
γ : Type ?u.42149
δ : Type ?u.42152
inst✝ : MeasurableSpace α
f g : α →ₛ β
⊢ ↑(piecewise ∅ (_ : MeasurableSet ∅) f g) = ↑g
simp
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.42149
δ : Type ?u.42152
inst✝ : MeasurableSpace α
f g : α →ₛ β
⊢ Set.piecewise ∅ ↑f ↑g = ↑g
convert Set.piecewise_empty f g