English
If α is covered by a countable open cover by sets whose subspaces are second-countable, then α is second-countable.
Русский
Если пространство покрыто счетным открытым покрытием, где каждый элемент покрытия образует вторично счетное подпространство, то всё пространство вторично счетно.
LaTeX
$$$[Countable ι] {U : ι \to Set(\alpha)}\ [\forall i, IsOpen(U(i))] (hc: ⋃ i, U(i) = \text{univ}) \Rightarrow SecondCountableTopology(\alpha)$$$
Lean4
/-- A countable open cover induces a second-countable topology if all open covers
are themselves second countable. -/
theorem secondCountableTopology_of_countable_cover {ι} [Countable ι] {U : ι → Set α}
[∀ i, SecondCountableTopology (U i)] (Uo : ∀ i, IsOpen (U i)) (hc : ⋃ i, U i = univ) : SecondCountableTopology α :=
haveI : IsTopologicalBasis (⋃ i, image ((↑) : U i → α) '' countableBasis (U i)) :=
isTopologicalBasis_of_cover Uo hc fun i => isBasis_countableBasis (U i)
this.secondCountableTopology (countable_iUnion fun _ => (countable_countableBasis _).image _)
