measurableSet_countableFiltration_of_mem

English

For each n, any s ∈ countablePartition α n is measurable in countableFiltration α n.

Русский

Для каждого n любое s ∈ countablePartition α n измеримо в countableFiltration α n.

LaTeX

$$$$ \MeasurableSet[countableFiltration \ α n](s) \quad \text{if } s \in countablePartition α n $$$$

Lean4

theorem measurableSet_countableFiltration_of_mem (n : ℕ) {s : Set α} (hs : s ∈ countablePartition α n) :
    MeasurableSet[countableFiltration α n] s :=
  measurableSet_generateFrom hs

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