aemeasurable_const_smul_iff — Mathlib

English

If c is a unit, then AEMeasurable (x ↦ c • f(x)) μ is equivalent to AEMeasurable f μ.

Русский

Если c является единицей, то AEMeasurable (λx. c • f(x)) μ эквивалентно AEMeasurable f μ.

LaTeX

$$$AEMeasurable (\\lambda x. c \\cdot f(x))\\mu \\iff AEMeasurable f\\mu$$$

Lean4

@[to_additive]
nonrec theorem aemeasurable_const_smul_iff {c : M} (hc : IsUnit c) :
    AEMeasurable (fun x => c • f x) μ ↔ AEMeasurable f μ :=
  let ⟨u, hu⟩ := hc
  hu ▸ aemeasurable_const_smul_iff u

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