div — Mathlib

English

If u and v are progMeasurable with group structure, then u i ω / v i ω is progMeasurable.

Русский

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

LaTeX

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

Lean4

@[to_additive]
protected theorem div [Group β] [ContinuousDiv β] (hu : ProgMeasurable f u) (hv : ProgMeasurable f v) :
    ProgMeasurable f fun i ω => u i ω / v i ω := fun i => (hu i).div (hv i)

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