apply_continuousLinearMap — Mathlib

English

If f is integrable on μ, then restricting μ to any set s preserves integrability.

Русский

Если f интегрируемо по μ, то ограничение меры μ на любое множество s сохраняет интегрируемость.

LaTeX

$$$ \\operatorname{Integrable}(f,\\mu) \\Rightarrow \\operatorname{Integrable}(f,\\mu\\restriction s) $$$

Lean4

theorem apply_continuousLinearMap {φ : α → H →SL[σ] E} (φ_int : Integrable φ μ) (v : H) :
    Integrable (fun a => φ a v) μ :=
  (ContinuousLinearMap.apply' E σ v).integrable_comp φ_int

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