no goals
α : Type u_1
β : Type u_2
γ : Type ?u.74519
δ : Type ?u.74522
δ' : Type ?u.74525
ι : Sort uι
s t u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : (x : α) → Decidable (x ∈ s)
f : ↑s → β
hf : Measurable f
g : ↑(sᶜ) → β
hg : Measurable g
hs : MeasurableSet s
⊢ Measurable (restrict s fun x => if hx : x ∈ s then f { val := x, property := hx } else g { val := x, property := hx })
simpa
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.74519
δ : Type ?u.74522
δ' : Type ?u.74525
ι : Sort uι
s t u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : (x : α) → Decidable (x ∈ s)
f : ↑s → β
hf : Measurable f
g : ↑(sᶜ) → β
hg : Measurable g
hs : MeasurableSet s
⊢ Measurable
    (restrict (sᶜ) fun x => if hx : x ∈ s then f { val := x, property := hx } else g { val := x, property := hx })
simpa