integral and linear maps

Stream: Is there code for X?

[Patrick Massot]

@Yury G. Kudryashov @Sebastien Gouezel Is there

lemma integral_linear_map {φ : α → E} {L : E →L[ℝ] F} (φ_meas : measurable φ)
  (φ_meas : integrable φ μ) : ∫ a, L (φ a) ∂μ = L (∫ a, φ a ∂μ)

somewhere?