coe_smul — Mathlib

English

Subtraction on simple functions passes to Lp via toLp: toLp(f-g) = toLp f - toLp g.

Русский

Векторное вычитание простых функций переносится во множества Lp: toLp(f-g) = toLp f - toLp g.

LaTeX

$$$\\mathrm{toLp}(f-g,\\,p,\\mu)=\\mathrm{toLp}(f,p,\\mu)-\\mathrm{toLp}(g,p,\\mu)$$$

Lean4

@[simp, norm_cast]
theorem coe_smul (c : 𝕜) (f : Lp.simpleFunc E p μ) : ((c • f : Lp.simpleFunc E p μ) : Lp E p μ) = c • (f : Lp E p μ) :=
  rfl

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