aemeasurable_prod — Mathlib

English

In a commutative monoid M, the a.e.-measurable property of a multiset product is preserved when each factor is a.e.-measurable.

Русский

В коммутативном моноиде M свойство a.e.-измеримости сохраняется при произведении множества факторов, каждое из которых a.e.-измеримо.

LaTeX

$$$AEMeasurable l.prod\\mu$ при $\\forall f \\in l, AEMeasurable f \\mu$$$

Lean4

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

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