mul — Mathlib

English

If f and g are measurable, then the pointwise product a ↦ f(a) · g(a) is measurable.

Русский

Если f и g измеримы, то точечное произведение a ↦ f(a) · g(a) измеримо.

LaTeX

$$$\\text{Measurable}(f) \\land \\text{Measurable}(g) \\Rightarrow \\text{Measurable}(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 : Measurable f) (hg : Measurable g) : Measurable fun a => f a * g a :=
  measurable_mul.comp (hf.prodMk hg)

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