borel_eq_generateFrom_Ici — Mathlib

English

In the same setting, the Borel σ-algebra on α is generated by all right-closed rays {x ∈ α | a ≤ x}, as a ranges over α.

Русский

В той же постановке борелевская сигма-алгебра на α порождается множествами {x ≥ a}, где a пробегает по α.

LaTeX

$$$\mathcal{B}(\alpha) = \sigma\bigl(\{[a, \infty) : a \in \alpha\}\bigr).$$$

Lean4

theorem borel_eq_generateFrom_Ici : borel α = MeasurableSpace.generateFrom (range Ici) :=
  @borel_eq_generateFrom_Iic αᵒᵈ _ _ _ _

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