smul_enorm — Mathlib

English

If f is integrable with values in ε, then c • f is integrable (ENorm context).

Русский

Если f интегрируема и принимает значения в ε, то c · f интегрируема (контекст ENorm).

LaTeX

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

Lean4

@[fun_prop]
theorem smul_enorm [NormedAddCommGroup 𝕜] [SMul 𝕜 ε] [ContinuousConstSMul 𝕜 ε] [ENormSMulClass 𝕜 ε] (c : 𝕜) {f : α → ε}
    (hf : Integrable f μ) : Integrable (c • f) μ := by constructor <;> fun_prop

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