English
If hf, hg are measurable as maps into β → M and h is a measurable map into β, then a ↦ (f(a) * g(a))(h(a)) is measurable.
Русский
Если f и g — измеримые семейства функций, а h — измеримая функция, то a ↦ (f(a) · g(a))(h(a)) измерима.
LaTeX
$$$\\text{Measurable}(f) \\Rightarrow \\text{Measurable}(g) \\Rightarrow \\text{Measurable}(a \\mapsto (f(a) \\star g(a))(h(a))).$$$
Lean4
/-- Compositional version of `Measurable.mul` for use by `fun_prop`. -/
@[to_additive (attr := fun_prop, aesop safe 20 apply (rule_sets := [Measurable])) /--
Compositional version of `Measurable.add` for use by `fun_prop`. -/
]
theorem mul' [MeasurableMul₂ M] {f g : α → β → M} {h : α → β} (hf : Measurable ↿f) (hg : Measurable ↿g)
(hh : Measurable h) : Measurable fun a ↦ (f a * g a) (h a) := by dsimp; fun_prop
