α : Type u_2
β : Type u_1
ι : Type ?u.1459789
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : { x // x ∈ kernel α β }
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x => x ∈ s
a : α
t : Set β
⊢ ↑↑(if a ∈ s then ↑κ a else ↑η a) t = if a ∈ s then ↑↑(↑κ a) t else ↑↑(↑η a) t
α : Type u_2
β : Type u_1
ι : Type ?u.1459789
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : { x // x ∈ kernel α β }
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x => x ∈ s
a : α
t : Set β
⊢ ↑↑(↑(piecewise hs κ η) a) t = if a ∈ s then ↑↑(↑κ a) t else ↑↑(↑η a) t
rw [piecewise_apply]
no goals
α : Type u_2
β : Type u_1
ι : Type ?u.1459789
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : { x // x ∈ kernel α β }
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x => x ∈ s
a : α
t : Set β
⊢ ↑↑(if a ∈ s then ↑κ a else ↑η a) t = if a ∈ s then ↑↑(↑κ a) t else ↑↑(↑η a) t
split_ifs <;> rfl