integrable_continuousLinearMap_prod'

English

If L is a continuous linear map on E×F→G and id maps are integrable, then L is integrable on μ×ν.

Русский

Пусть L – непрерывное линейное отображение E×F→G, и интегрируемы соответствующие карты; тогда L интегрируемо по μ×ν.

LaTeX

$$$$\\text{Integrable } L\\; (μ×ν)$$$$

Lean4

theorem integrable_continuousLinearMap_prod' (hLμ : Integrable (L.comp (.inl ℝ E F)) μ)
    (hLν : Integrable (L.comp (.inr ℝ E F)) ν) : Integrable L (μ.prod ν) :=
  by
  change Integrable (fun v ↦ L v) (μ.prod ν)
  simp_rw [← L.comp_inl_add_comp_inr]
  exact (hLμ.comp_fst ν).add (hLν.comp_snd μ)

Похожие утверждения