mul_const — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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