English
A finite-dimensional manifold modeled on a locally compact field is locally compact; the local compactness of the base field and the target model transfer to the manifold.
Русский
Конечномерное многообразие, моделируемое на локально компактном поле, локально компактно; локальная компактность базового поля и целевой модели переносится на многообразие.
LaTeX
$$$\text{Manifold.locallyCompact_of_finiteDimensional} (I : ModelWithCorners 𝕜 E H) [LocallyCompactSpace 𝕜] [FiniteDimensional 𝕜 E] : LocallyCompactSpace M$$$
Lean4
/-- A finite-dimensional manifold modelled on a locally compact field
(such as ℝ, ℂ or the `p`-adic numbers) is locally compact. -/
theorem locallyCompact_of_finiteDimensional (I : ModelWithCorners 𝕜 E H) [LocallyCompactSpace 𝕜]
[FiniteDimensional 𝕜 E] : LocallyCompactSpace M :=
by
have : ProperSpace E := FiniteDimensional.proper 𝕜 E
have : LocallyCompactSpace H := I.locallyCompactSpace
exact ChartedSpace.locallyCompactSpace H M
