English
Let f: α → 𝕜 and g: α → β be functions such that f is strongly measurable and g is strongly measurable, where 𝕜 acts on β via a continuous scalar action. Then the pointwise product x ↦ f(x) • g(x) is strongly measurable.
Русский
Пусть f: α → 𝕜 и g: α → β — функции, причём f является сильно измеримой, а g — сильно измеримой, причем 𝕜 действует на β через непрерывное скалярное действие. Тогда функция x ↦ f(x) • g(x) сильно измерима.
LaTeX
$$$\forall f: \alpha \to 𝕜 \ ; \forall g: \alpha \to β, \ (\text{StronglyMeasurable } f) \land (\text{StronglyMeasurable } g) \Rightarrow \text{StronglyMeasurable } (x \mapsto f(x) \;•\; g(x))$$$
Lean4
@[to_additive (attr := fun_prop, aesop safe 20 apply (rule_sets := [Measurable]))]
protected theorem smul {𝕜} [TopologicalSpace 𝕜] [SMul 𝕜 β] [ContinuousSMul 𝕜 β] {f : α → 𝕜} {g : α → β}
(hf : StronglyMeasurable f) (hg : StronglyMeasurable g) : StronglyMeasurable fun x => f x • g x :=
continuous_smul.comp_stronglyMeasurable (hf.prodMk hg)
