Lean4
theorem borel_eq_generateFrom_Ico_mem_aux {α : Type*} [TopologicalSpace α] [LinearOrder α] [OrderTopology α]
[SecondCountableTopology α] {s : Set α} (hd : Dense s) (hbot : ∀ x, IsBot x → x ∈ s)
(hIoo : ∀ x y : α, x < y → Ioo x y = ∅ → y ∈ s) :
borel α = .generateFrom {S : Set α | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ico l u = S} :=
by
set S : Set (Set α) := {S | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ico l u = S}
refine le_antisymm ?_ (generateFrom_Ico_mem_le_borel _ _)
letI : MeasurableSpace α := generateFrom S
rw [borel_eq_generateFrom_Iio]
refine generateFrom_le (forall_mem_range.2 fun a => ?_)
rcases hd.exists_countable_dense_subset_bot_top with ⟨t, hts, hc, htd, htb, -⟩
by_cases ha : ∀ b < a, (Ioo b a).Nonempty
· convert_to MeasurableSet (⋃ (l ∈ t) (u ∈ t) (_ : l < u) (_ : u ≤ a), Ico l u)
· ext y
simp only [mem_iUnion, mem_Iio, mem_Ico]
constructor
· intro hy
rcases htd.exists_le' (fun b hb => htb _ hb (hbot b hb)) y with ⟨l, hlt, hly⟩
rcases htd.exists_mem_open isOpen_Ioo (ha y hy) with ⟨u, hut, hyu, hua⟩
exact ⟨l, hlt, u, hut, hly.trans_lt hyu, hua.le, hly, hyu⟩
· rintro ⟨l, -, u, -, -, hua, -, hyu⟩
exact hyu.trans_le hua
· refine MeasurableSet.biUnion hc fun a ha => MeasurableSet.biUnion hc fun b hb => ?_
refine MeasurableSet.iUnion fun hab => MeasurableSet.iUnion fun _ => ?_
exact .basic _ ⟨a, hts ha, b, hts hb, hab, mem_singleton _⟩
· simp only [not_forall, not_nonempty_iff_eq_empty] at ha
replace ha : a ∈ s := hIoo ha.choose a ha.choose_spec.fst ha.choose_spec.snd
convert_to MeasurableSet (⋃ (l ∈ t) (_ : l < a), Ico l a)
· symm
simp only [← Ici_inter_Iio, ← iUnion_inter, inter_eq_right, subset_def, mem_iUnion, mem_Ici, mem_Iio]
intro x hx
rcases htd.exists_le' (fun b hb => htb _ hb (hbot b hb)) x with ⟨z, hzt, hzx⟩
exact ⟨z, hzt, hzx.trans_lt hx, hzx⟩
· refine .biUnion hc fun x hx => MeasurableSet.iUnion fun hlt => ?_
exact .basic _ ⟨x, hts hx, a, ha, hlt, mem_singleton _⟩
