smul — Mathlib

English

If f is IntegrableAtFilter, then c·f is IntegrableAtFilter for any scalar c.

Русский

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

LaTeX

$$$\\forall c,\\ \\operatorname{IntegrableAtFilter}(f, l, \\mu) \\Rightarrow \\operatorname{IntegrableAtFilter}(c \\cdot f, l, \\mu).$$$

Lean4

protected theorem smul {𝕜 : Type*} [NormedAddCommGroup 𝕜] [SMulZeroClass 𝕜 E] [IsBoundedSMul 𝕜 E] {f : α → E}
    (hf : IntegrableAtFilter f l μ) (c : 𝕜) : IntegrableAtFilter (c • f) l μ :=
  by
  rcases hf with ⟨s, sl, hs⟩
  exact ⟨s, sl, hs.smul c⟩

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