mul_const — Mathlib

English

Multiplication by a constant on the right preserves strong measurability.

Русский

Умножение на константу справа сохраняет сильную измеримость.

LaTeX

$$$\text{StronglyMeasurable}(f) \Rightarrow \forall c,\ \text{StronglyMeasurable}(x \mapsto f(x) \cdot c)$$$

Lean4

@[to_additive (attr := fun_prop, measurability)]
theorem mul_const [Mul β] [ContinuousMul β] (hf : StronglyMeasurable f) (c : β) : StronglyMeasurable fun x => f x * c :=
  hf.mul stronglyMeasurable_const

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