toLp_const_smul — Mathlib

English

Scaling inside the function and scaling inside the Lp representative commute: multiplying a function by a scalar and then taking its Lp representative equals multiplying the Lp representative by that scalar.

Русский

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

LaTeX

$$$\text{toLp}\ (c\cdot f)\ (hf) = c\cdot (\text{toLp}\ f)$$$

Lean4

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

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