eq_borel_upgradeStandardBorel — Mathlib

English

For any α, a standard measurable space structure is equivalent to the Borel sets of its upgraded standard Borel space.

Русский

Для любого α структура пространства меры совпадает с борелевыми множествами обновленного пространства стандартных Борелевых множеств.

LaTeX

$$$ ‹\mathcal{M}→› = \mathrm{borel}(\mathrm{upgradeStandardBorel}(α)) $$$

Lean4

/-- The `MeasurableSpace α` instance on a `StandardBorelSpace` `α` is equal to
the Borel sets of `upgradeStandardBorel α`. -/
theorem eq_borel_upgradeStandardBorel [MeasurableSpace α] [StandardBorelSpace α] :
    ‹MeasurableSpace α› = @borel _ (upgradeStandardBorel α).toTopologicalSpace :=
  @BorelSpace.measurable_eq _ (upgradeStandardBorel α).toTopologicalSpace _ (upgradeStandardBorel α).toBorelSpace

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