English
Let M be a locally compact, nonempty topological space that is modeled on a normed space E via a model with corners I. Then the model space E is locally compact.
Русский
Пусть M является локально компактным непустым топологическим пространством, моделируемым на нормированном пространстве E с помощью модели с углами I. Тогда пространство E является локально компактным.
LaTeX
$$$$ [Nonempty\ M] \wedge [LocallyCompactSpace\ M] \Rightarrow LocallyCompactSpace\ E $$$$
Lean4
/-- A locally compact manifold must be modelled on a locally compact space. -/
theorem of_locallyCompact_manifold (I : ModelWithCorners 𝕜 E H) [h : Nonempty M] [LocallyCompactSpace M] :
LocallyCompactSpace E := by
rcases h with ⟨x⟩
obtain ⟨y, hy⟩ := interior_extChartAt_target_nonempty I x
have h'y : y ∈ (extChartAt I x).target := interior_subset hy
obtain ⟨s, hmem, hss, hcom⟩ :=
LocallyCompactSpace.local_compact_nhds ((extChartAt I x).symm y) (extChartAt I x).source
((isOpen_extChartAt_source x).mem_nhds ((extChartAt I x).map_target h'y))
have : IsCompact <| (extChartAt I x) '' s := hcom.image_of_continuousOn <| (continuousOn_extChartAt x).mono hss
apply this.locallyCompactSpace_of_mem_nhds_of_addGroup (x := y)
rw [← (extChartAt I x).right_inv h'y]
apply extChartAt_image_nhds_mem_nhds_of_mem_interior_range (PartialEquiv.map_target (extChartAt I x) h'y) _ hmem
simp only [(extChartAt I x).right_inv h'y]
exact interior_mono (extChartAt_target_subset_range x) hy
