mul — Mathlib

English

If f and g are almost everywhere measurable, then the map a ↦ f(a) · g(a) is almost everywhere measurable.

Русский

Если f и g почти всюду измеримы, то 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 (fun a => f a * g a) μ :=
  measurable_mul.comp_aemeasurable (hf.prodMk hg)

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