fun_const_smul — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive (attr := fun_prop, measurability)]
theorem fun_const_smul (hg : AEMeasurable g μ) (c : M) : AEMeasurable (c • g ·) μ :=
  (measurable_const_smul c).comp_aemeasurable hg

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