toLp_smul — Mathlib

English

Scaling a simple function and then passing to the Lp construction is the same as passing the function to Lp and then scaling the result.

Русский

Умножение простой функции на скаляр и затем отображение в Lp эквивалентно отображению в Lp и последующему умножению на скаляр.

LaTeX

$$$toLp(c\cdot f) = c\cdot toLp(f)\quad\text{(for }f\text{ with } MemLp f\,p\,\mu\text{)}$$$

Lean4

theorem toLp_smul (f : α →ₛ E) (hf : MemLp f p μ) (c : 𝕜) : toLp (c • f) (hf.const_smul c) = c • toLp f hf :=
  rfl

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