mul_const — Mathlib

English

If f is almost everywhere measurable, then x ↦ f(x) · c is almost everywhere measurable for any fixed c.

Русский

Если f измеримо почти всюду, то x ↦ f(x) · c измеримо почти всюду.

LaTeX

$$$\\text{AEMeasurable}(f,\\mu) \\Rightarrow \\forall c, \\; \\text{AEMeasurable}(x \\mapsto f(x) \\cdot c, \\mu).$$$

Lean4

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

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