generateFrom_countableGeneratingSet

English

The generated sigma-algebra by the countable generating set equals the given measurable space.

Русский

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

LaTeX

$$$ \text{generateFrom}(\text{countableGeneratingSet}(\alpha)) = m $$$

Lean4

theorem generateFrom_countableGeneratingSet [m : MeasurableSpace α] [h : CountablyGenerated α] :
    generateFrom (countableGeneratingSet α) = m :=
  (generateFrom_insert_empty _).trans <| h.isCountablyGenerated.choose_spec.2.symm

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