stronglyMeasurable_le — Mathlib

English

If i ≤ j, then the i-th component is strongly measurable with respect to the j-th stage of the filtration.

Русский

Если i ≤ j, то i-й компонент адаптирован и сильно измерим относительно j-й стадии фильтрации.

LaTeX

$$$$ \\forall i,j, \\ i \\le j \\Rightarrow \\mathrm{StronglyMeasurable}_{f_j}(u_i) $$$$

Lean4

theorem stronglyMeasurable_le {i j : ι} (hf : Adapted f u) (hij : i ≤ j) : StronglyMeasurable[f j] (u i) :=
  (hf i).mono (f.mono hij)

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