opensMeasurable — Mathlib

English

In a Borel space, all open sets are measurable.

Русский

В борелевом пространстве все открытые множества измеримы.

LaTeX

$$$$ \text{OpensMeasurableSpace }(\alpha) \text{ holds when } \alpha \text{ is a BorelSpace}. $$$$

Lean4

/-- In a `BorelSpace` all open sets are measurable. -/
instance (priority := 100) opensMeasurable {α : Type*} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] :
    OpensMeasurableSpace α :=
  ⟨ge_of_eq <| BorelSpace.measurable_eq⟩

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