mul' — Mathlib

English

If hf and hg are almost everywhere measurable, then aemulbling them coordinatewise yields AEMeasurable of the product: a ↦ f(a) * g(a).

Русский

Если hf и hg — AЭ-измеримые, то частью множения является AЭ-измеримая функция a ↦ f(a)·g(a).

LaTeX

$$$\\text{AEMeasurable}(f) \\Rightarrow \\text{AEMeasurable}(g) \\Rightarrow \\text{AEMeasurable}(a \\mapsto f(a) \\cdot g(a)).$$$

Lean4

@[to_additive (attr := fun_prop, aesop safe 20 apply (rule_sets := [Measurable]))]
theorem mul' [MeasurableMul₂ M] (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) : AEMeasurable (f * g) μ :=
  measurable_mul.comp_aemeasurable (hf.prodMk hg)

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