borel_eq_top_of_discrete — Mathlib

English

If α has a discrete topology, then borel α equals the top measurable space.

Русский

Если у α дискретная топология, то борельево пространство измеримых является тождением верхнего измеримого пространства.

LaTeX

$$$\mathrm{borel}(\alpha) = \top$$$

Lean4

theorem borel_eq_top_of_discrete [TopologicalSpace α] [DiscreteTopology α] : borel α = ⊤ :=
  top_le_iff.1 fun s _ => GenerateMeasurable.basic s (isOpen_discrete s)

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