borel_eq_top_of_countable — Mathlib

English

On a countable T0 space, the Borel sigma-algebra is the top (i.e., all sets are measurable).

Русский

На счётном T0-пространстве борелевская сигма-алгебра равна верхнему элементу, то есть все множества измеримы.

LaTeX

$$$\\text{borel}(\\alpha) = ⊤$ for countable T0 spaces.$$

Lean4

theorem borel_eq_top_of_countable {α : Type*} [TopologicalSpace α] [T0Space α] [Countable α] : borel α = ⊤ :=
  by
  refine top_unique fun s _ ↦ ?_
  borelize α
  exact .of_discrete

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