stronglyMeasurable — Mathlib

English

For any adapted family f and index i, the i-th component u(i) is strongly measurable with respect to the base sigma-algebra.

Русский

Для любой адаптированной последовательности f компоненту i можно считать сильно измеримой относительно базовой сигма-алгебры.

LaTeX

$$$$ \\forall i, \\ \\text{StronglyMeasurable}_m(u_i) $$$$

Lean4

protected theorem stronglyMeasurable {i : ι} (hf : Adapted f u) : StronglyMeasurable[m] (u i) :=
  (hf i).mono (f.le i)

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