const_mul — Mathlib

English

Multiplication by a constant on the right also preserves MemLp, i.e., f · c belongs to MemLp if f does.

Русский

Умножение на константу слева сохраняет MemLp, то есть f · c принадлежит MemLp если f принадлежит.

LaTeX

$$$\operatorname{MemLp}(f,p,μ) \Rightarrow \operatorname{MemLp}(f\cdot c,p,μ)$$$

Lean4

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

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