English
Let α be a space with an open cover U_i, and for each i a collection b_i of subsets of U_i forming a topological basis for the subspace U_i. Then the union over i of the images of b_i in α is a topological basis for α.
Русский
Пусть α — пространство, покрытое открытыми множествами U_i. Пусть для каждого i множество b_i является топологическим базисом для подпространства U_i. Тогда объединение образов b_i в α образует топологический базис для α.
LaTeX
$$$\\mathsf{IsTopologicalBasis}\\left(\\bigcup_{i} \\mathrm{image}(\\iota_i)(b_i)\\right)$$$
Lean4
theorem isTopologicalBasis_of_cover {ι} {U : ι → Set α} (Uo : ∀ i, IsOpen (U i)) (Uc : ⋃ i, U i = univ)
{b : ∀ i, Set (Set (U i))} (hb : ∀ i, IsTopologicalBasis (b i)) :
IsTopologicalBasis (⋃ i : ι, image ((↑) : U i → α) '' b i) :=
by
refine isTopologicalBasis_of_isOpen_of_nhds (fun u hu => ?_) ?_
· simp only [mem_iUnion, mem_image] at hu
rcases hu with ⟨i, s, sb, rfl⟩
exact (Uo i).isOpenMap_subtype_val _ ((hb i).isOpen sb)
· intro a u ha uo
rcases iUnion_eq_univ_iff.1 Uc a with ⟨i, hi⟩
lift a to ↥(U i) using hi
rcases (hb i).exists_subset_of_mem_open ha (uo.preimage continuous_subtype_val) with ⟨v, hvb, hav, hvu⟩
exact ⟨(↑) '' v, mem_iUnion.2 ⟨i, mem_image_of_mem _ hvb⟩, mem_image_of_mem _ hav, image_subset_iff.2 hvu⟩
