borel_eq_generateFrom_Ico — Mathlib

English

If s is dense with boundary properties, borel α equals the generateFrom of Ioc l u with l,u∈s.

Русский

Если s плотна и удовлетворяет граничным свойствам, борелова алгебра равна generateFrom{Ioc l u}.

LaTeX

$$$\text{borel }\alpha = \generateFrom\{S\mid ∃l∈s, ∃u∈s, l

Lean4

theorem borel_eq_generateFrom_Ico (α : Type*) [TopologicalSpace α] [SecondCountableTopology α] [LinearOrder α]
    [OrderTopology α] : borel α = .generateFrom {S : Set α | ∃ (l u : α), l < u ∧ Ico l u = S} := by
  simpa only [exists_prop, mem_univ, true_and] using
    (@dense_univ α _).borel_eq_generateFrom_Ico_mem_aux (fun _ _ => mem_univ _) fun _ _ _ _ => mem_univ _

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