Theorem: integral_funSplitAt_right (ForML/IndexIntegral.lean)

State before:
ι : Type u_1
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
mE : MeasureSpace E
inst✝⁶ : SigmaFinite volume
D : ι → Type u_3
inst✝⁵ : (i : ι) → NormedAddCommGroup (D i)
inst✝⁴ : (i : ι) → NormedSpace ℝ (D i)
mD : (i : ι) → MeasureSpace (D i)
inst✝³ : ∀ (i : ι), SigmaFinite volume
F : Type u_4
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
i : ι
f : (ι → E) → F
hf : Integrable f
⊢ ∫ (x : ι → E), f x = ∫ (x : { j // j ≠ i } → E) (u : E), f ((Equiv.funSplitAt i E).symm (u, x))
Tactic:
exact integral_piSplitAt_right i hf
State after:
no goals