smul_measure — Mathlib

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⟩

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