measurableSet_filtrationOfSet' — Mathlib

English

For a sequence of sets s_i that are measurable, then s_i is measurable in filtrationOfSet hsm i.

Русский

Для последовательности множеств s_i, где каждое измеримо, s_i измеримо в filtrationOfSet hsm i.

LaTeX

$$$\\forall i,\\; MeasurableSet[filtrationOfSet hsm i](s_i)$$$

Lean4

theorem measurableSet_filtrationOfSet' {s : ι → Set Ω} (hsm : ∀ n, MeasurableSet[m] (s n)) (i : ι) :
    MeasurableSet[filtrationOfSet hsm i] (s i) :=
  measurableSet_filtrationOfSet hsm i le_rfl

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