smul_const — Mathlib

English

If f is strongly measurable, then the function x ↦ f(x) • c is strongly measurable for any fixed c.

Русский

Если f — сильно измеримая, то функция x ↦ f(x) • c также является сильно измеримой для фиксированного c.

LaTeX

$$$\forall f: \alpha \to 𝕜, \text{StronglyMeasurable } f \Rightarrow \forall c, \text{StronglyMeasurable } (x \mapsto f(x) \;•\; c)$$$

Lean4

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

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