generateFrom_iUnion_countablePartition

English

The sigma-algebra generated by the union of all countable partitions equals the given measurable space m: generateFrom (⋃ n, countablePartition α n) = m.

Русский

Сигма-алгебра, порождаемая объединением всех countablePartition α n, равна данным измеримым множествам: generateFrom(⋃n countablePartition α n) = m.

LaTeX

$$$$ \\operatorname{generateFrom}\\Big(\\bigcup_{n} \\text{countablePartition } \\alpha n\\Big) = m. $$$$

Lean4

theorem generateFrom_iUnion_countablePartition (α : Type*) [m : MeasurableSpace α] [CountablyGenerated α] :
    generateFrom (⋃ n, countablePartition α n) = m := by
  rw [countablePartition, generateFrom_iUnion_memPartition,
    range_enumerateCountable_of_mem _ empty_mem_countableGeneratingSet, generateFrom_countableGeneratingSet]

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