measurableSet_partitionFiltration_of_mem

English

If ht is a family of measurable sets (ht n = MeasurableSet (t n)) then for every n and every a, the set memPartitionSet t n a is measurable with respect to the nth filtration.

Русский

Пусть ht — семейство измеримых множеств (ht n = MeasurableSet (t n)). Тогда для каждого n и каждого a множество memPartitionSet t n a измеримо в n-й фильтрации.

LaTeX

$$$$ \forall n,\ MeasurableSet(t n) \Rightarrow \MeasurableSet[partitionFiltration(ht)\,n](memPartitionSet(t,n,a)) $$$$

Lean4

theorem measurableSet_partitionFiltration_of_mem (ht : ∀ n, MeasurableSet (t n)) (n : ℕ) {s : Set α}
    (hs : s ∈ memPartition t n) : MeasurableSet[partitionFiltration ht n] s :=
  measurableSet_generateFrom hs

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