measurableSet_filtrationOfSet — Mathlib

English

For a sequence of sets s_i that are each measurable, and any index i, if j ≤ i then s_j is measurable in filtrationOfSet hsm i.

Русский

Если множества s_i измеримы, то для любого i и любого j ≤ i множество s_j измеримо в filtrationOfSet hsm i.

LaTeX

$$$\\forall i \\forall j \\; (j \\le i) \\Rightarrow MeasurableSet[filtrationOfSet hsm i](s_j)$$$

Lean4

theorem measurableSet_filtrationOfSet {s : ι → Set Ω} (hsm : ∀ i, MeasurableSet[m] (s i)) (i : ι) {j : ι} (hj : j ≤ i) :
    MeasurableSet[filtrationOfSet hsm i] (s j) :=
  MeasurableSpace.measurableSet_generateFrom ⟨j, hj, rfl⟩

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