aestronglyMeasurable_const_smul_iff₀

English

If c ≠ 0 in a multiplicative group with zero, AEStronglyMeasurable (c • f) μ is equivalent to AEStronglyMeasurable f μ.

Русский

Если c ≠ 0 в группе с нулём, то AEStronglyMeasurable(c • f) эквивалентно AEStronglyMeasurable f.

LaTeX

$$$\text{Ne}(c,0) \Rightarrow \left( \text{AEStronglyMeasurable}(c \cdot f, μ) \iff \text{AEStronglyMeasurable}(f, μ) \right).$$$

Lean4

theorem _root_.aestronglyMeasurable_const_smul_iff₀ {c : G₀} (hc : c ≠ 0) :
    AEStronglyMeasurable (fun x => c • f x) μ ↔ AEStronglyMeasurable f μ :=
  (IsUnit.mk0 _ hc).aestronglyMeasurable_const_smul_iff

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