const_smul' — Mathlib

English

If hf is strongly measurable, then the function x ↦ c • f x is strongly measurable for any constant c.

Русский

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

LaTeX

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

Lean4

@[to_additive (attr := fun_prop, measurability)]
protected theorem const_smul' {𝕜} [SMul 𝕜 β] [ContinuousConstSMul 𝕜 β] (hf : StronglyMeasurable f) (c : 𝕜) :
    StronglyMeasurable fun x => c • f x :=
  hf.const_smul c

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