countablyGenerated_of_standardBorel

English

If α is a standard Borel space, then its measurable space is countably generated.

Русский

Если α — стандартное Борелево пространство, то борелево-мера α порождается счётно.

LaTeX

$$$ \text{MeasurableSpace.CountablyGenerated}(α) $$$

Lean4

instance (priority := 100) countablyGenerated_of_standardBorel [StandardBorelSpace α] :
    MeasurableSpace.CountablyGenerated α :=
  letI := upgradeStandardBorel α
  inferInstance

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