mul_const — Mathlib

English

If f ∈ MemLp, then the product f · c (or c · f) is MemLp for any scalar c.

Русский

Если f ∈ MemLp, то произведение f на константу сохраняет принадлежность MemLp для любого скаляра c.

LaTeX

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

Lean4

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

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