English
Riesz’s theorem for manifolds: if a locally compact manifold M is modeled on E with model I, and the scalar field 𝕜 is complete, then E is finite-dimensional provided M is nonempty.
Русский
Теорема Рiesz для многообразий: если локально компактное многообразие M моделировано на пространство E с помощью модели I, и поле 𝕜 является полным, то пространство E конечномерно, если M непусто.
LaTeX
$$$$ [CompleteSpace\ 𝕜] \wedge [Nonempty\ M] \wedge [LocallyCompactSpace\ M] \Rightarrow FiniteDimensional\ 𝕜\ E $$$$
Lean4
/-- Riesz's theorem applied to manifolds: a locally compact manifolds must be modelled on a
finite-dimensional space. This is the converse to `Manifold.locallyCompact_of_finiteDimensional`. -/
theorem of_locallyCompact_manifold [CompleteSpace 𝕜] (I : ModelWithCorners 𝕜 E H) [Nonempty M] [LocallyCompactSpace M] :
FiniteDimensional 𝕜 E := by
have := LocallyCompactSpace.of_locallyCompact_manifold M I
exact FiniteDimensional.of_locallyCompactSpace 𝕜
