stronglyMeasurable_prod — Mathlib

English

For a multiset of functions, each strongly measurable, the function mapping x to the product of the list values at x is strongly measurable.

Русский

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

LaTeX

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

Lean4

@[to_additive (attr := fun_prop, measurability)]
theorem _root_.Multiset.stronglyMeasurable_prod (l : Multiset (α → M)) (hl : ∀ f ∈ l, StronglyMeasurable f) :
    StronglyMeasurable l.prod := by
  rcases l with ⟨l⟩
  simpa using l.stronglyMeasurable_prod (by simpa using hl)

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