measurable_cylinderEvents_lambda — Mathlib

English

A function f: α → ∀ i, X_i is measurable with respect to cylinderEvents Δ if and only if each coordinate component f(a) i is measurable for i ∈ Δ.

Русский

Функция f: α → ∀ i, X_i измерима относительно cylinderEvents Δ тогда и только тогда, когда каждая координатная часть f(a)_i измерима для i ∈ Δ.

LaTeX

$$$\\text{measurable\\_cylinderEvents\\_lambda} (f : α \\to ∀ i, X_i) \\iff \\ ∀ i, \\ i \\in Δ \\to Measurable(\\lambda a. f(a,i))$$$

Lean4

@[fun_prop, aesop safe 100 apply (rule_sets := [Measurable])]
theorem measurable_cylinderEvents_lambda (f : α → ∀ i, X i) (hf : ∀ i, Measurable fun a ↦ f a i) : Measurable f :=
  measurable_pi_iff.mpr hf

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