English
If u is an open cover of X and each B_i is a topological basis for the topology on u_i, then the union over i of the images of B_i under the inclusion into X is a topological basis for the union of the subspace topologies.
Русский
Если u — открытое покрытие X, и для каждого i база B_i является базисом топологии на подпространстве u_i, то объединение образов B_i в X образует базис топологии для объединения подпространств.
LaTeX
$$$\mathrm{IsOpenCover}(u) \land (\forall i, \mathrm{IsTopologicalBasis}(B_i)) \rightarrow \mathrm{IsTopologicalBasis}\bigl(\bigcup_i (\mathrm{Subtype.val} \,'\,' B_i)\bigr)$$$
Lean4
theorem isTopologicalBasis (hu : IsOpenCover u) {B : ∀ i, Set (Set (u i))} (hB : ∀ i, IsTopologicalBasis (B i)) :
IsTopologicalBasis (⋃ i, (Subtype.val '' ·) '' B i) :=
isTopologicalBasis_of_cover (fun i ↦ (u i).2) hu.iSup_set_eq_univ hB
