mul — Mathlib

English

If u and v are progressively measurable, then their pointwise product is progressively measurable.

Русский

Если u и v прогрессивно измеримы, то их покомпонентное произведение тоже прогрессивно измеримо.

LaTeX

$$$\\mathrm{ProgMeasurable}(f,u) \\land \\mathrm{ProgMeasurable}(f,v) \\Rightarrow \\mathrm{ProgMeasurable}(f, (\\lambda i\\,\\omega. u i\\omega \\cdot v i\\omega))$$$

Lean4

@[to_additive]
protected theorem mul [Mul β] [ContinuousMul β] (hu : ProgMeasurable f u) (hv : ProgMeasurable f v) :
    ProgMeasurable f fun i ω => u i ω * v i ω := fun i => (hu i).mul (hv i)

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