const_smul — Mathlib

English

For any scalar 𝕜 with continuous scalar multiplication, AEStronglyMeasurable f μ implies AEStronglyMeasurable (c • f) μ for any c.

Русский

Для любого скаляра c с непрерывным скалярным умножением, если f— AEStronglyMeasurable по μ, то c•f — тоже AEStronglyMeasurable по μ.

LaTeX

$$$\forall c, \text{AEStronglyMeasurable}(c \cdot f, μ) \Leftarrow \text{AEStronglyMeasurable}(f, μ).$$$

Lean4

@[measurability]
protected theorem const_smul {𝕜} [TopologicalSpace 𝕜] [Zero β] [SMulZeroClass 𝕜 β] [ContinuousSMul 𝕜 β]
    (hf : AEFinStronglyMeasurable f μ) (c : 𝕜) : AEFinStronglyMeasurable (c • f) μ :=
  ⟨c • hf.mk f, hf.finStronglyMeasurable_mk.const_smul c, hf.ae_eq_mk.const_smul c⟩

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