measurableSet_partitionFiltration_memPartitionSet

English

For ht and n, memPartitionSet t n is a measurable subset of the nth filtration.

Русский

Для ht и n множество memPartitionSet t n является измеримым подмножеством n-й фильтрации.

LaTeX

$$$$ \Measurable \mathrm{(partitionFiltration}\; ht\; n) \; (memPartitionSet\; t\; n) $$$$

Lean4

theorem measurableSet_partitionFiltration_memPartitionSet (ht : ∀ n, MeasurableSet (t n)) (n : ℕ) (a : α) :
    MeasurableSet[partitionFiltration ht n] (memPartitionSet t n a) :=
  measurableSet_partitionFiltration_of_mem ht n (memPartitionSet_mem t n a)

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