borel_eq_generateFrom_Ioc_mem_aux

English

Analogous borel generation for Ico with density assumptions.

Русский

Аналогично for Ico при плотностных предположениях.

LaTeX

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

Lean4

theorem borel_eq_generateFrom_Ioc_mem_aux {α : Type*} [TopologicalSpace α] [LinearOrder α] [OrderTopology α]
    [SecondCountableTopology α] {s : Set α} (hd : Dense s) (hbot : ∀ x, IsTop x → x ∈ s)
    (hIoo : ∀ x y : α, x < y → Ioo x y = ∅ → x ∈ s) :
    borel α = .generateFrom {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ioc l u = S} :=
  by
  convert hd.orderDual.borel_eq_generateFrom_Ico_mem_aux hbot fun x y hlt he => hIoo y x hlt _ using 2
  · ext s
    constructor <;> rintro ⟨l, hl, u, hu, hlt, rfl⟩
    exacts [⟨u, hu, l, hl, hlt, Ico_toDual⟩, ⟨u, hu, l, hl, hlt, Ioc_toDual⟩]
  · erw [Ioo_toDual]
    exact he

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