generateFrom_Ico_mem_le_borel — Mathlib

English

The sigma-algebra generated by sets of the form Ico l u with l ∈ s, u ∈ t (and l < u) is contained in the borel algebra on α.

Русский

Сигма‑алгебра, порождаемая множествами Ico l u с l∈s, u∈t, l<u, включена в борелеву алгебру на α.

LaTeX

$$$\mathsf{generateFrom}\{S\mid ∃l∈s, ∃u∈t, l

Lean4

theorem generateFrom_Ico_mem_le_borel {α : Type*} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α]
    (s t : Set α) : MeasurableSpace.generateFrom {S | ∃ l ∈ s, ∃ u ∈ t, l < u ∧ Ico l u = S} ≤ borel α :=
  by
  apply generateFrom_le
  borelize α
  rintro _ ⟨a, -, b, -, -, rfl⟩
  exact measurableSet_Ico

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