Theorem: ContinuousMultilinearMap.integral_apply (ForML/MultilinearIntegral.lean)

State before:
α : Type u_1
inst✝¹⁰ : MeasurableSpace α
inst✝⁹ : TopologicalSpace α
inst✝⁸ : OpensMeasurableSpace α
inst✝⁷ : SecondCountableTopology α
ι : Type u_2
inst✝⁶ : Fintype ι
ι' : Type u_3
inst✝⁵ : Fintype ι'
D : ι → Type u_4
inst✝⁴ : (i : ι) → NormedAddCommGroup (D i)
inst✝³ : (i : ι) → NormedSpace ℝ (D i)
F : Type u_5
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
c : α → ContinuousMultilinearMap ℝ D F
μ : Measure α
hc : Integrable c
m : (i : ι) → D i
⊢ ∫ (x : α), (c x) m ∂μ = (∫ (x : α), c x ∂μ) m
Tactic:
simpa using ContinuousLinearMap.integral_comp_comm (apply ℝ D F m) hc
State after:
no goals