English
If f is AEMeasurable with respect to μ, then for any scalar c, f is AEMeasurable with respect to c • μ.
Русский
Если f — AЕ-измеримая относительно μ, то при любом скалярном коэффициенте c функция f остается AЕ-измеримой относительно c • μ.
LaTeX
$$$\mathrm{AEMeasurable}(f, \mu) \rightarrow \forall c, \mathrm{AEMeasurable}(f, c \cdot \mu)$$$
Lean4
@[measurability]
theorem smul_measure [SMul R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞] (h : AEMeasurable f μ) (c : R) :
AEMeasurable f (c • μ) :=
⟨h.mk f, h.measurable_mk, ae_smul_measure h.ae_eq_mk c⟩