English
If each α_i has a basis B_i of opens, then the sigma-construct of opens across the family is a basis of opens on the disjoint sum.
Русский
Если каждая часть пространства имеет базис открытых множеств B_i, то база открытых множеств над сигма‑суммой является базисом открытых множеств над объединением.
LaTeX
$$$\operatorname{IsBasis}\left( \bigcup_{i} \{ \Sigma i '' U : U \in B_i \} \right)$$$
Lean4
theorem isBasis_sigma {ι : Type*} {α : ι → Type*} [∀ i, TopologicalSpace (α i)] {B : ∀ i, Set (Opens (α i))}
(hB : ∀ i, IsBasis (B i)) : IsBasis (⋃ i : ι, (fun U ↦ ⟨Sigma.mk i '' U.1, isOpenMap_sigmaMk _ U.2⟩) '' B i) :=
by
convert TopologicalSpace.IsTopologicalBasis.sigma hB
simp only [IsBasis, Set.image_iUnion, ← Set.image_comp]
simp
