measurable_smul_const — Mathlib

English

Let c ∈ E with c ≠ 0 be fixed. For f: α → 𝕜, the function x ↦ f(x)·c is measurable if and only if f is measurable.

Русский

Пусть фиксированно c ∈ E, c ≠ 0. Тогда функция x ↦ f(x)·c измерима тогда и только тогда, когда f: α → 𝕜 измерима.

LaTeX

$$$c \\neq 0 \\Rightarrow \\bigl(\\text{Measurable}(x \\mapsto f(x) c) \\iff \\text{Measurable}(x \\mapsto f(x))\\bigr).$$$

Lean4

theorem measurable_smul_const {f : α → 𝕜} {c : E} (hc : c ≠ 0) : (Measurable fun x => f x • c) ↔ Measurable f :=
  (isClosedEmbedding_smul_left hc).measurableEmbedding.measurable_comp_iff

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