English
In a second-countable space, there exists a countable subfamily of a given basis that still generates the topology.
Русский
В пространстве второй счетности существует счетное подмножество базиса, которое всё ещё порождает топологию.
LaTeX
$$$[SecondCountableTopology\ α] (ht : IsTopologicalBasis t) : ∃ s ⊆ t, s.Countable ∧ IsTopologicalBasis s$$$
Lean4
/-- In a disjoint union space `Σ i, E i`, one can form a topological basis by taking the union of
topological bases on each of the parts of the space. -/
theorem sigma {s : ∀ i : ι, Set (Set (E i))} (hs : ∀ i, IsTopologicalBasis (s i)) :
IsTopologicalBasis (⋃ i : ι, (fun u => (Sigma.mk i '' u : Set (Σ i, E i))) '' s i) :=
by
refine .of_hasBasis_nhds fun a ↦ ?_
rw [Sigma.nhds_eq]
convert (((hs a.1).nhds_hasBasis).map _).to_image_id
aesop
