stronglyMeasurable_prod — Mathlib

English

Compositional version for Finset: strongly measurable of the product applied to a measurable g is preserved.

Русский

Композиционная версия для Finset: сохранение сильной измеримости при применении произведения к измеримой g.

LaTeX

$$$\forall s:\text{Finset } ι, \ (\forall i \in s, \text{StronglyMeasurable } ↿(f i)) \text{ and } \text{Measurable } g \Rightarrow \text{StronglyMeasurable } (a \mapsto (\prod_{i \in s} f i a)(g a))$$$

Lean4

@[to_additive (attr := measurability, fun_prop)]
theorem _root_.Finset.stronglyMeasurable_prod {ι : Type*} {f : ι → α → M} (s : Finset ι)
    (hf : ∀ i ∈ s, StronglyMeasurable (f i)) : StronglyMeasurable (∏ i ∈ s, f i) :=
  Finset.prod_induction _ _ (fun _a _b ha hb => ha.mul hb) (@stronglyMeasurable_one α M _ _ _) hf

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