const_mul — Mathlib

English

If f is AEStronglyMeasurable, then the function x ↦ c·f(x) is AEStronglyMeasurable for any constant c.

Русский

Если f является AEStronglyMeasurable, то функция x ↦ c·f(x) является AEStronglyMeasurable для любого константного c.

LaTeX

$$$AEStronglyMeasurable\ f\ μ \rightarrow \forall c, AEStronglyMeasurable\left(x \mapsto c\, f(x)\right) μ$$$

Lean4

@[to_additive (attr := fun_prop, measurability)]
protected theorem const_mul [Mul β] [ContinuousMul β] (hf : AEStronglyMeasurable[m] f μ) (c : β) :
    AEStronglyMeasurable[m] (fun x => c * f x) μ :=
  aestronglyMeasurable_const.mul hf

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