const_smul — Mathlib

English

If f is strongly measurable, then multiplying f by a constant c (on the left) yields a strongly measurable function c • f.

Русский

Если f — сильно измеримая, то умножение ее на константу c слева, то есть c • f, также сильно измеримо.

LaTeX

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

Lean4

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

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