stronglyMeasurable_prod — Mathlib

English

A list of functions, each strongly measurable, yields a strongly measurable function given by mapping x to the product of the list values at x.

Русский

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

LaTeX

$$$\forall l: \text{List}(\alpha \to M), \ (\forall f \in l, \text{StronglyMeasurable } f) \Rightarrow \text{StronglyMeasurable } (\lambda a, \prod_{f \in l} f(a))$$$

Lean4

@[to_additive (attr := fun_prop, measurability)]
theorem _root_.List.stronglyMeasurable_prod (l : List (α → M)) (hl : ∀ f ∈ l, StronglyMeasurable f) :
    StronglyMeasurable l.prod := by
  induction l with
  | nil => exact stronglyMeasurable_one
  | cons f l ihl =>
    rw [List.forall_mem_cons] at hl
    rw [List.prod_cons]
    exact hl.1.mul (ihl hl.2)

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