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, (\\lambda i\\,a. \\prod_{c\\in s} U c i a))$$$

Lean4

@[to_additive]
protected theorem finset_prod {γ} [CommMonoid β] [ContinuousMul β] {U : γ → ι → Ω → β} {s : Finset γ}
    (h : ∀ c ∈ s, ProgMeasurable f (U c)) : ProgMeasurable f fun i a => ∏ c ∈ s, U c i a := by
  convert ProgMeasurable.finset_prod' h using 1; ext (i a); simp only [Finset.prod_apply]

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