measurable_const_smul_iff — Mathlib

English

If c is a unit, then measurability of the function x ↦ c • f(x) is equivalent to measurability of f. This holds for any measurable structure where c is a unit.

Русский

Если c является единицей, то измеримость функции x ↦ c • f(x) эквивалентна измеримости f.

LaTeX

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

Lean4

@[to_additive]
nonrec theorem measurable_const_smul_iff {c : M} (hc : IsUnit c) : (Measurable fun x => c • f x) ↔ Measurable f :=
  let ⟨u, hu⟩ := hc
  hu ▸ measurable_const_smul_iff u

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