instBorelSpace — Mathlib

English

If α is countable and carries the appropriate measurable and topological structures, then α is a BorelSpace.

Русский

Если α — счетное пространство с подходящими измеримостными и топологическими структурами, то оно является Борелевым пространством.

LaTeX

$$$$ \text{BorelSpace}(\alpha) $$$$

Lean4

instance instBorelSpace [Countable α] [MeasurableSpace α] [MeasurableSingletonClass α] [TopologicalSpace α]
    [DiscreteTopology α] : BorelSpace α :=
  by
  have : ∀ s, @MeasurableSet α inferInstance s := fun s ↦ s.to_countable.measurableSet
  have : ∀ s, @MeasurableSet α (borel α) s := fun s ↦ measurableSet_generateFrom (isOpen_discrete s)
  exact ⟨by aesop⟩

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