stronglyMeasurable_fun_prod — Mathlib

English

The product over a finite multiset of strongly measurable functions is strongly measurable.

Русский

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

LaTeX

$$$\forall l:\text{Multiset}(\alpha \to M), \ (\forall f \in l, \text{StronglyMeasurable } f) \Rightarrow \text{StronglyMeasurable } (l.prod)$$

Lean4

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

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