mul_const — Mathlib

English

If f is measurable and c is fixed, the map x ↦ f(x) · c is measurable.

Русский

Если f измерима и фиксированное число c, то x ↦ f(x) · c измеримо.

LaTeX

$$$\\text{Measurable}(f) \\Rightarrow \\text{Measurable}(x \\mapsto f(x) \\cdot c).$$$

Lean4

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

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