aemeasurable_const_smul_iff₀ — Mathlib

English

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

Русский

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

LaTeX

$$$(\\text{IsUnit } c) \\Rightarrow (\\text{AEMeasurable } (\\lambda x. c \\cdot f(x)) \\mu \\iff \\text{AEMeasurable } f \\mu)$$$

Lean4

theorem aemeasurable_const_smul_iff₀ {c : G₀} (hc : c ≠ 0) : AEMeasurable (fun x => c • f x) μ ↔ AEMeasurable f μ :=
  (IsUnit.mk0 c hc).aemeasurable_const_smul_iff

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