const_smul — Mathlib

English

If f: α → 𝕜 is AEStronglyMeasurable, then ∀ c, the map x ↦ c • f(x) is AEStronglyMeasurable.

Русский

Если f: α → 𝕜 является AEStronglyMeasurable, тогда ∀ c, отображение x ↦ c • f(x) является AEStronglyMeasurable.

LaTeX

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

Lean4

@[to_additive (attr := fun_prop, measurability)]
protected theorem const_smul {𝕜} [SMul 𝕜 β] [ContinuousConstSMul 𝕜 β] (hf : AEStronglyMeasurable[m] f μ) (c : 𝕜) :
    AEStronglyMeasurable[m] (c • f) μ :=
  ⟨c • hf.mk f, hf.stronglyMeasurable_mk.const_smul c, hf.ae_eq_mk.const_smul c⟩

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