stronglyMeasurable_fun_prod — Mathlib

English

Finite set of strongly measurable functions yields a strongly measurable function given by the product over the set at each point.

Русский

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

LaTeX

$$$\forall s:\text{Finset } ι, \ (\forall i \in s, \text{StronglyMeasurable } (f i)) \Rightarrow \text{StronglyMeasurable } (a \mapsto \prod_{i \in s} f i a)$$$

Lean4

@[to_additive (attr := measurability, fun_prop)]
theorem _root_.Finset.stronglyMeasurable_fun_prod {ι : Type*} {f : ι → α → M} (s : Finset ι)
    (hf : ∀ i ∈ s, StronglyMeasurable (f i)) : StronglyMeasurable fun a => ∏ i ∈ s, f i a := by
  simpa only [← Finset.prod_apply] using s.stronglyMeasurable_prod hf

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