aemeasurable_smul_measure_iff — Mathlib

English

For c ≠ 0, AEMeasurable f (c • μ) is equivalent to AEMeasurable f μ.

Русский

При c ≠ 0: AЕ-измеримая f относительно c•μ эквивалентна AЕ-измеримости f относительно μ.

LaTeX

$$$\mathrm{AEMeasurable}(f, c \cdot \mu) \iff \mathrm{AEMeasurable}(f, \mu)$, \text{for } c \neq 0$$

Lean4

@[simp]
theorem aemeasurable_smul_measure_iff {c : ℝ≥0∞} (hc : c ≠ 0) : AEMeasurable f (c • μ) ↔ AEMeasurable f μ :=
  ⟨fun h => ⟨h.mk f, h.measurable_mk, (ae_smul_measure_iff hc).1 h.ae_eq_mk⟩, fun h =>
    ⟨h.mk f, h.measurable_mk, (ae_smul_measure_iff hc).2 h.ae_eq_mk⟩⟩

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