English
Let α be a linearly ordered topological space with a countable basis and the order topology. Then the Borel σ-algebra on α is generated by all left-closed rays {x ∈ α | x ≤ a}, as a ranges over α.
Русский
Пусть α — линейно упорядоченное топологическое пространство с счётной базой и порядком вершины. Борелевская сигма-алгебра на α порождается множествами {x ≤ a}, где a пробегает по α.
LaTeX
$$$\mathcal{B}(\alpha) = \sigma\bigl(\{(-\infty, a] : a \in \alpha\}\bigr)$.$$
Lean4
theorem borel_eq_generateFrom_Iic : borel α = MeasurableSpace.generateFrom (range Iic) :=
by
rw [borel_eq_generateFrom_Ioi]
refine le_antisymm ?_ ?_
· refine MeasurableSpace.generateFrom_le fun t ht => ?_
obtain ⟨u, rfl⟩ := ht
rw [← compl_Iic]
exact (MeasurableSpace.measurableSet_generateFrom (mem_range.mpr ⟨u, rfl⟩)).compl
· refine MeasurableSpace.generateFrom_le fun t ht => ?_
obtain ⟨u, rfl⟩ := ht
rw [← compl_Ioi]
exact (MeasurableSpace.measurableSet_generateFrom (mem_range.mpr ⟨u, rfl⟩)).compl
