smul — Mathlib

English

If [MeasurableSMul₂ M X] and f,g are measurable, then the pointwise smul x ↦ f(x) • g(x) is measurable.

Русский

Если есть измеримое двумерное действие SMul и функции f,g измеримы, то точечное произведение x ↦ f(x) • g(x) измеримо.

LaTeX

$$$\text{Measurable } f \land \text{Measurable } g \Rightarrow \text{Measurable}(\lambda x. f(x) \cdot g(x))$$$

Lean4

@[to_additive (attr := fun_prop, aesop safe 20 apply (rule_sets := [Measurable]))]
theorem smul [MeasurableSMul₂ M X] (hf : Measurable f) (hg : Measurable g) : Measurable fun x => f x • g x :=
  measurable_smul.comp (hf.prodMk hg)

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