const_mul — Mathlib

English

Let M be a type with a measurable space and a multiplication. If f: α → M is measurable, then for every fixed c ∈ M the map x ↦ c · f(x) is measurable.

Русский

Пусть M обладает структурой измеримости и умножением. Если f: α → M измерима, то для любого фиксированного c ∈ M функция x ↦ c · f(x) измерима.

LaTeX

$$$\\text{Measurable}(f) \\;\\Rightarrow\\; \\forall c \\in M,\\; \\text{Measurable}(x \\mapsto c \\cdot f(x)).$$$

Lean4

@[to_additive (attr := fun_prop, measurability)]
theorem const_mul [MeasurableMul M] (hf : Measurable f) (c : M) : Measurable fun x => c * f x :=
  (measurable_const_mul c).comp hf

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