fun_smul_enorm — Mathlib

English

If f is integrable, then x ↦ c • f(x) is integrable in ENorm setting.

Русский

Если f интегрируема, то x ↦ c · f(x) интегрируема в контексте ENorm.

LaTeX

$$$\mathrm{Integrable}\left(f,\mu\right) \Rightarrow \mathrm{Integrable}\left(x \mapsto c \cdot f(x)\right).$$$

Lean4

theorem fun_smul_enorm [NormedAddCommGroup 𝕜] [SMul 𝕜 ε] [ContinuousConstSMul 𝕜 ε] [ENormSMulClass 𝕜 ε] (c : 𝕜)
    {f : α → ε} (hf : Integrable f μ) : Integrable (fun x ↦ c • f x) μ :=
  hf.smul_enorm c

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