const_mul' — Mathlib

English

If f ∈ Lp, then the function x ↦ c · f(x) is in Lp for any scalar c.

Русский

Если f ∈ Lp, то функция x ↦ c · f(x) принадлежит Lp для любого скаляра c.

LaTeX

$$$\\\\text{MemLp}(f, p, \\mu) \\\\Rightarrow \\\\text{MemLp}(x \\mapsto c \\cdot f(x), p, \\mu) \\\\text{ for all } c \\\\in \\\\mathbb{K}$$$

Lean4

theorem const_mul' {f : α → 𝕜} (hf : MemLp f p μ) (c : 𝕜) : MemLp (fun x => c * f x) p μ :=
  hf.const_smul c

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