const_smul — Mathlib

English

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

Русский

Если g — AEMеасurable, то отображение x ↦ c • g(x) является AEMеасurable.

LaTeX

$$$\text{AEMeasurable}(g) \Rightarrow \forall c, \text{AEMeasurable}(x \mapsto c\cdot g(x))$$$

Lean4

@[to_additive (attr := fun_prop, measurability)]
theorem const_smul (hf : AEMeasurable g μ) (c : M) : AEMeasurable (c • g) μ :=
  hf.fun_const_smul c

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