stronglyMeasurable_fun_prod — Mathlib

English

Finite set product of strongly measurable functions is strongly measurable.

Русский

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

LaTeX

$$$\forall s:\text{Finset } ι, \ (\forall i \in s, \text{StronglyMeasurable } (f i)) \Rightarrow \text{StronglyMeasurable } (s.prod (f))$$$

Lean4

@[to_additive (attr := fun_prop, measurability)]
theorem _root_.Multiset.stronglyMeasurable_fun_prod (s : Multiset (α → M)) (hs : ∀ f ∈ s, StronglyMeasurable f) :
    StronglyMeasurable fun x => (s.map fun f : α → M => f x).prod := by
  simpa only [← Pi.multiset_prod_apply] using s.stronglyMeasurable_prod hs

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