α : Type u_3
β : Type u_2
ι : Type ?u.1471684
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : { x // x ∈ kernel α β }
s : Set α
hs : MeasurableSet s
inst✝³ : DecidablePred fun x => x ∈ s
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
a : α
g : β → E
⊢ (∫ (b : β), g b ∂if a ∈ s then ↑κ a else ↑η a) = if a ∈ s then ∫ (b : β), g b ∂↑κ a else ∫ (b : β), g b ∂↑η a
α : Type u_3
β : Type u_2
ι : Type ?u.1471684
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : { x // x ∈ kernel α β }
s : Set α
hs : MeasurableSet s
inst✝³ : DecidablePred fun x => x ∈ s
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
a : α
g : β → E
⊢ (∫ (b : β), g b ∂↑(piecewise hs κ η) a) = if a ∈ s then ∫ (b : β), g b ∂↑κ a else ∫ (b : β), g b ∂↑η a
simp_rw [piecewise_apply]
no goals
α : Type u_3
β : Type u_2
ι : Type ?u.1471684
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : { x // x ∈ kernel α β }
s : Set α
hs : MeasurableSet s
inst✝³ : DecidablePred fun x => x ∈ s
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
a : α
g : β → E
⊢ (∫ (b : β), g b ∂if a ∈ s then ↑κ a else ↑η a) = if a ∈ s then ∫ (b : β), g b ∂↑κ a else ∫ (b : β), g b ∂↑η a
split_ifs <;> rfl