English
If a charted space M has a countable cover of chart sources that covers all M, then M is second-countable.
Русский
Если пространство charted имеет счетное покрытие источников карт, которые покрывают всё M, то M вторично счётно.
LaTeX
$$SecondCountableTopology M := ChartedSpace.secondCountable_of_countable_cover ...$$
Lean4
/-- If a topological space admits an atlas with locally compact charts, then the space itself
is locally compact. -/
theorem locallyCompactSpace [LocallyCompactSpace H] : LocallyCompactSpace M :=
by
have :
∀ x : M,
(𝓝 x).HasBasis (fun s ↦ s ∈ 𝓝 (chartAt H x x) ∧ IsCompact s ∧ s ⊆ (chartAt H x).target) fun s ↦
(chartAt H x).symm '' s :=
fun x ↦ by
rw [← (chartAt H x).symm_map_nhds_eq (mem_chart_source H x)]
exact ((compact_basis_nhds (chartAt H x x)).hasBasis_self_subset (chart_target_mem_nhds H x)).map _
refine .of_hasBasis this ?_
rintro x s ⟨_, h₂, h₃⟩
exact h₂.image_of_continuousOn ((chartAt H x).continuousOn_symm.mono h₃)
