English
In a disjoint union space, one can form a topological basis by taking the union of topological bases on each component.
Русский
В дизъюнктивном разложении пространство образует базис как объединение базисов отдельных компонент.
LaTeX
$$$IsTopologicalBasis( Set.iUnion (fun i => Set.image (fun u => Set.image (Sigma.mk i) u) (s_i)) )$$$
Lean4
/-- In a sum space `α ⊕ β`, one can form a topological basis by taking the union of
topological bases on each of the two components. -/
theorem sum {s : Set (Set α)} (hs : IsTopologicalBasis s) {t : Set (Set β)} (ht : IsTopologicalBasis t) :
IsTopologicalBasis ((fun u => Sum.inl '' u) '' s ∪ (fun u => Sum.inr '' u) '' t) :=
by
apply isTopologicalBasis_of_isOpen_of_nhds
· rintro u (⟨w, hw, rfl⟩ | ⟨w, hw, rfl⟩)
· exact IsOpenEmbedding.inl.isOpenMap w (hs.isOpen hw)
· exact IsOpenEmbedding.inr.isOpenMap w (ht.isOpen hw)
· rintro (x | x) u hxu u_open
· obtain ⟨v, vs, xv, vu⟩ : ∃ v ∈ s, x ∈ v ∧ v ⊆ Sum.inl ⁻¹' u :=
hs.exists_subset_of_mem_open hxu (isOpen_sum_iff.1 u_open).1
exact ⟨Sum.inl '' v, mem_union_left _ (mem_image_of_mem _ vs), mem_image_of_mem _ xv, image_subset_iff.2 vu⟩
· obtain ⟨v, vs, xv, vu⟩ : ∃ v ∈ t, x ∈ v ∧ v ⊆ Sum.inr ⁻¹' u :=
ht.exists_subset_of_mem_open hxu (isOpen_sum_iff.1 u_open).2
exact ⟨Sum.inr '' v, mem_union_right _ (mem_image_of_mem _ vs), mem_image_of_mem _ xv, image_subset_iff.2 vu⟩
