const_smul' — Mathlib

English

The same as smul but with a slightly different formulation; constant smul via the prime version.

Русский

Аналогично smul, но через версию со смещенным определением.

LaTeX

$$$\text{smul'}\ f\mu \Rightarrow \forall c, AEStronglyMeasurable\left(x \mapsto c \bullet f(x)\right) μ$$$

Lean4

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

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