borel_eq_generateFrom_Ico_mem — Mathlib

English

As above, but with Ioc l u intervals.

Русский

Аналогично, но с интервалами Ioc l u.

LaTeX

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

Lean4

theorem borel_eq_generateFrom_Ico_mem {α : Type*} [TopologicalSpace α] [LinearOrder α] [OrderTopology α]
    [SecondCountableTopology α] [DenselyOrdered α] [NoMinOrder α] {s : Set α} (hd : Dense s) :
    borel α = .generateFrom {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ico l u = S} :=
  hd.borel_eq_generateFrom_Ico_mem_aux (by simp) fun _ _ hxy H => ((nonempty_Ioo.2 hxy).ne_empty H).elim

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