English
If H is second-countable and there is a countable collection s of points in M whose chart sources cover all of M, then M is second-countable.
Русский
Если H вторично счётно, и существует счётное покрытие M редактором карт chartAt H x, то M тоже вторично счётно.
LaTeX
$$$[\text{SecondCountableTopology } H] \Rightarrow (\exists s: Set M, \#s < \infty, \bigcup_{x\in s} (chartAt H x).source = \mathsf{univ})\Rightarrow \operatorname{SecondCountableTopology} M$$$
Lean4
theorem secondCountable_of_countable_cover [SecondCountableTopology H] {s : Set M}
(hs : ⋃ (x) (_ : x ∈ s), (chartAt H x).source = univ) (hsc : s.Countable) : SecondCountableTopology M :=
by
haveI : ∀ x : M, SecondCountableTopology (chartAt H x).source := fun x ↦
(chartAt (H := H) x).secondCountableTopology_source
haveI := hsc.toEncodable
rw [biUnion_eq_iUnion] at hs
exact secondCountableTopology_of_countable_cover (fun x : s ↦ (chartAt H (x : M)).open_source) hs
