smul — Mathlib

English

If f is locally integrable with respect to μ, then for every scalar c, the function c • f is locally integrable with respect to μ.

Русский

Если f локально интегрируема по μ, то для любого скаляра c функция c • f локально интегрируема по μ.

LaTeX

$$$\operatorname{LocallyIntegrable}(f, \mu) \Rightarrow \forall c\, \operatorname{LocallyIntegrable}(c\cdot f, \mu)$$$

Lean4

protected theorem smul {f : X → E} {𝕜 : Type*} [NormedAddCommGroup 𝕜] [SMulZeroClass 𝕜 E] [IsBoundedSMul 𝕜 E]
    (hf : LocallyIntegrable f μ) (c : 𝕜) : LocallyIntegrable (c • f) μ := fun x ↦ (hf x).smul c

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