finset_prod' — Mathlib

English

Finite product of ProgMeasurable functions is ProgMeasurable.

Русский

Конечная произведение прогрессивно измеримых функций также прогрессивно измеримо.

LaTeX

$$$(\\forall c \\in s,\\ \\mathrm{ProgMeasurable}(f, U c)) \\Rightarrow \\mathrm{ProgMeasurable}(f, \\prod_{c \\in s} U c)$$$

Lean4

@[to_additive]
protected theorem finset_prod' {γ} [CommMonoid β] [ContinuousMul β] {U : γ → ι → Ω → β} {s : Finset γ}
    (h : ∀ c ∈ s, ProgMeasurable f (U c)) : ProgMeasurable f (∏ c ∈ s, U c) :=
  Finset.prod_induction U (ProgMeasurable f) (fun _ _ => ProgMeasurable.mul) (progMeasurable_const _ 1) h

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