# Commit 2020-09-18 21:57 0269a76e

View on Github →feat(integration): integral commutes with continuous linear maps (#4167) from the sphere eversion project. Main result:

```
continuous_linear_map.integral_apply_comm {α : Type*} [measurable_space α] {μ : measure α}
{E : Type*} [normed_group E] [second_countable_topology E] [normed_space ℝ E] [complete_space E]
[measurable_space E] [borel_space E] {F : Type*} [normed_group F]
[second_countable_topology F] [normed_space ℝ F] [complete_space F]
[measurable_space F] [borel_space F]
{φ : α → E} (L : E →L[ℝ] F) (φ_meas : measurable φ) (φ_int : integrable φ μ) :
∫ a, L (φ a) ∂μ = L (∫ a, φ a ∂μ)
```