α : Type u_1
β : Type u_2
γ : Type ?u.39189
δ : Type ?u.39192
inst✝ : MeasurableSpace α
f g : α →ₛ β
⊢ Set.piecewise univ ↑f ↑g = ↑f
α : Type u_1
β : Type u_2
γ : Type ?u.39189
δ : Type ?u.39192
inst✝ : MeasurableSpace α
f g : α →ₛ β
⊢ ↑(piecewise univ (_ : MeasurableSet univ) f g) = ↑f
simp
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.39189
δ : Type ?u.39192
inst✝ : MeasurableSpace α
f g : α →ₛ β
⊢ Set.piecewise univ ↑f ↑g = ↑f
convert Set.piecewise_univ f g