mul — Mathlib

English

If f and g are AEStronglyMeasurable, then their pointwise product f(x)·g(x) is AEStronglyMeasurable.

Русский

Пусть f и g — AEStronglyMeasurable; тогда точечное произведение f(x)·g(x) также AEStronglyMeasurable.

LaTeX

$$$AEStronglyMeasurable\ f\ μ \rightarrow AEStronglyMeasurable\ g\ μ \rightarrow AEStronglyMeasurable\left(x \mapsto f(x)\, g(x)\right) μ$$$

Lean4

@[to_additive (attr := fun_prop, aesop safe 20 apply (rule_sets := [Measurable]))]
protected theorem mul [Mul β] [ContinuousMul β] (hf : AEStronglyMeasurable[m] f μ) (hg : AEStronglyMeasurable[m] g μ) :
    AEStronglyMeasurable[m] (f * g) μ :=
  ⟨hf.mk f * hg.mk g, by fun_prop, hf.ae_eq_mk.mul hg.ae_eq_mk⟩

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