measurable_prod — Mathlib

English

For a commutative monoid M, the product over a multiset of functions is a measurable function provided each function is measurable.

Русский

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

LaTeX

$$$\\text{Measurable } l.prod$ для $l : \\text{Multiset}(\\alpha \\to M)$, $\\forall f \\in l, \\text{Measurable } f$$$

Lean4

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

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