generateFrom_natGeneratingSequence

English

The sigma-algebra generated by the range of natGeneratingSequence equals the given measurable space.

Русский

Сигма-алгебра, порождённая образами natGeneratingSequence, равна заданному измеримому пространству.

LaTeX

$$$ \text{generateFrom}(\text{range}(\text{natGeneratingSequence}(\alpha))) = m $$$

Lean4

theorem generateFrom_natGeneratingSequence (α : Type*) [m : MeasurableSpace α] [CountablyGenerated α] :
    generateFrom (range (natGeneratingSequence _)) = m := by
  rw [natGeneratingSequence, range_enumerateCountable_of_mem _ empty_mem_countableGeneratingSet,
    generateFrom_countableGeneratingSet]

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