English
In a suitably nice ordered space, the Borel sigma-algebra equals the sigma-algebra generated by the half-open intervals Iio a.
Русский
В подходящем упорядоченном пространстве бин to Боре́ль—алгебра равна алгебре, порождённой полупроизвольными интервалами Iio a.
LaTeX
$$$\\text{borel}(\\alpha) = \\mathrm{generateFrom}(\\{ Iio(a) : a \\in \\alpha\\})$$$
Lean4
theorem borel_eq_generateFrom_Iio : borel α = .generateFrom (range Iio) :=
by
refine le_antisymm ?_ (generateFrom_le ?_)
· rw [borel_eq_generateFrom_of_subbasis (@OrderTopology.topology_eq_generate_intervals α _ _ _)]
letI : MeasurableSpace α := MeasurableSpace.generateFrom (range Iio)
have H : ∀ a : α, MeasurableSet (Iio a) := fun a => GenerateMeasurable.basic _ ⟨_, rfl⟩
refine generateFrom_le ?_
rintro _ ⟨a, rfl | rfl⟩
· rcases em (∃ b, a ⋖ b) with ⟨b, hb⟩ | hcovBy
· rw [hb.Ioi_eq, ← compl_Iio]
exact (H _).compl
· rcases isOpen_biUnion_countable (Ioi a) Ioi fun _ _ ↦ isOpen_Ioi with ⟨t, hat, htc, htU⟩
have : Ioi a = ⋃ b ∈ t, Ici b :=
by
refine Subset.antisymm ?_ <| iUnion₂_subset fun b hb ↦ Ici_subset_Ioi.2 (hat hb)
refine Subset.trans ?_ <| iUnion₂_mono fun _ _ ↦ Ioi_subset_Ici_self
simpa [CovBy, htU, subset_def] using hcovBy
simp only [this, ← compl_Iio]
exact .biUnion htc <| fun _ _ ↦ (H _).compl
· apply H
· rw [forall_mem_range]
intro a
exact GenerateMeasurable.basic _ isOpen_Iio
