English
If the topology is generated from a subbasis s, then borel α equals generateFrom s.
Русский
Если топология генерируется по подбазе s, тогда борельево пространство измеримых равно generateFrom s.
LaTeX
$$$\mathrm{borel}(\alpha) = \mathrm{generateFrom}(s)$$$
Lean4
theorem borel_eq_generateFrom_of_subbasis {s : Set (Set α)} [t : TopologicalSpace α] [SecondCountableTopology α]
(hs : t = .generateFrom s) : borel α = .generateFrom s :=
le_antisymm
(generateFrom_le fun u (hu : t.IsOpen u) => by
rw [hs] at hu
induction hu with
| basic u hu => exact GenerateMeasurable.basic u hu
| univ => exact @MeasurableSet.univ α (generateFrom s)
| inter s₁ s₂ _ _ hs₁ hs₂ => exact @MeasurableSet.inter α (generateFrom s) _ _ hs₁ hs₂
| sUnion f hf ih =>
rcases isOpen_sUnion_countable f (by rwa [hs]) with ⟨v, hv, vf, vu⟩
rw [← vu]
exact @MeasurableSet.sUnion α (generateFrom s) _ hv fun x xv => ih _ (vf xv))
(generateFrom_le fun u hu =>
GenerateMeasurable.basic _ <| show t.IsOpen u by rw [hs]; exact GenerateOpen.basic _ hu)
