smul_const — Mathlib

English

If g is AEMeasurable, then the map x ↦ c • g(x) is AEMeasurable for any fixed c.

Русский

Если g AЕMeasurable, то отображение x ↦ c • g(x) является AЕMeasurable для любого фиксированного c.

LaTeX

$$$\text{AЕMeasurable}(g) \Rightarrow \forall c, \text{AЕMeasurable}(x \mapsto c\cdot g(x))$$$

Lean4

@[to_additive (attr := fun_prop, measurability)]
theorem smul_const (hf : AEMeasurable f μ) (y : X) : AEMeasurable (fun x => f x • y) μ :=
  (MeasurableSMul.measurable_smul_const y).comp_aemeasurable hf

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