borel_eq_generateFrom_Ioc_mem — Mathlib

English

Analogous borel generation for Ioc with density assumptions.

Русский

Аналогично для Ioc при плотности.

LaTeX

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

Lean4

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

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