mul — Mathlib

English

If f and g are strongly measurable, then the pointwise product f·g is strongly measurable.

Русский

Если f и g сильно измеримы, то их произведение по точкам сохраняет сильную измеримость.

LaTeX

$$$\text{StronglyMeasurable}(f) \land \text{StronglyMeasurable}(g) \Rightarrow \text{StronglyMeasurable}(x \mapsto f(x) \cdot g(x))$$$

Lean4

@[to_additive (attr := fun_prop, aesop safe 20 apply (rule_sets := [Measurable]))]
protected theorem mul [Mul β] [ContinuousMul β] (hf : StronglyMeasurable f) (hg : StronglyMeasurable g) :
    StronglyMeasurable (f * g) :=
  ⟨fun n => hf.approx n * hg.approx n, fun x => (hf.tendsto_approx x).mul (hg.tendsto_approx x)⟩

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