const_mul — Mathlib

English

If f is almost everywhere measurable, then the map x ↦ c · f(x) is also almost everywhere measurable for any fixed c ∈ M.

Русский

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

LaTeX

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

Lean4

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

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