stronglyMeasurable_const_smul_iff₀

English

If c ≠ 0 in a group with zero, then (StronglyMeasurable (c • f)) ↔ StronglyMeasurable f.

Русский

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

LaTeX

$$$\forall f, c \neq 0 \Rightarrow (\text{StronglyMeasurable } (x \mapsto c \;•\; f(x)) \iff \text{StronglyMeasurable } f)$$$

Lean4

theorem _root_.stronglyMeasurable_const_smul_iff₀ {_ : MeasurableSpace α} {c : G₀} (hc : c ≠ 0) :
    (StronglyMeasurable fun x => c • f x) ↔ StronglyMeasurable f :=
  (IsUnit.mk0 _ hc).stronglyMeasurable_const_smul_iff

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