smul_add — Mathlib

English

Holder respects left scalar multiplication: B.holder r (c•f) g = c•B.holder r f g.

Русский

Holder сохраняет левое умножение на скаляр: holder(r, B, c f, g) = c holder(r, B, f, g).

LaTeX

$$$\\mathrm{holder}(r,B,c\\cdot f,g) = c\\cdot \\mathrm{holder}(r,B,f,g).$$$

Lean4

protected theorem smul_add (f₁ f₂ : Lp 𝕜 p μ) (g : Lp E q μ) : (f₁ + f₂) • g = f₁ • g + f₂ • g :=
  by
  simp only [smul_def, ← MemLp.toLp_add]
  apply MemLp.toLp_congr
  filter_upwards [AEEqFun.coeFn_add f₁.val f₂.val] with x hx
  simp [hx, add_smul]

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