toBorelSpace — Mathlib

English

A space with discrete topology has the Borel sigma-algebra equal to its full measurable sigma-algebra, hence is a Borel space.

Русский

Пространство с дискретной топологией имеет борелеву сигма-алгебру, равную полной алгебре измеримости, следовательно, является пространством Бореля.

LaTeX

$$(DiscreteTopology\, α) \\Rightarrow BorelSpace\, α$$

Lean4

instance toBorelSpace {α : Type*} [TopologicalSpace α] [DiscreteTopology α] [MeasurableSpace α]
    [DiscreteMeasurableSpace α] : BorelSpace α := by constructor; ext;
  simp [MeasurableSpace.measurableSet_generateFrom, MeasurableSet.of_discrete]

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