smul_const — Mathlib

English

If f: α → 𝕜 and c is a fixed β, then the map x ↦ f(x) • c is AEStronglyMeasurable.

Русский

Если f: α → 𝕜 и константа c, то x ↦ f(x) • c AEStronglyMeasurable.

LaTeX

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

Lean4

@[to_additive (attr := fun_prop, measurability)]
protected theorem smul_const {𝕜} [TopologicalSpace 𝕜] [SMul 𝕜 β] [ContinuousSMul 𝕜 β] {f : α → 𝕜}
    (hf : AEStronglyMeasurable[m] f μ) (c : β) : AEStronglyMeasurable[m] (fun x => f x • c) μ :=
  continuous_smul.comp_aestronglyMeasurable (hf.prodMk aestronglyMeasurable_const)

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