measurable_const_smul_iff₀ — Mathlib

English

For any c ∈ M, if c is a unit, then the map x ↦ c • f(x) is measurable if and only if f is measurable.

Русский

Для любого c ∈ M, если c является единицей, то отображение x ↦ c • f(x) измеримо тогда и только тогда, когда f измеримо.

LaTeX

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

Lean4

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

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