of_locallyCompact_module — Mathlib

English

A locally compact normed vector space is finite-dimensional over 𝕜.

Русский

Локально компактное нормированное векторное пространство над 𝕜 является конечномерным.

LaTeX

$$$[LocallyCompactSpace E] \\\\Rightarrow FiniteDimensional 𝕜 E$$$

Lean4

theorem of_locallyCompact_module [Nontrivial E] [LocallyCompactSpace E] : ProperSpace 𝕜 :=
  have : LocallyCompactSpace 𝕜 := by
    obtain ⟨v, hv⟩ : ∃ v : E, v ≠ 0 := exists_ne 0
    let L : 𝕜 → E := fun t ↦ t • v
    have : IsClosedEmbedding L := isClosedEmbedding_smul_left hv
    apply IsClosedEmbedding.locallyCompactSpace this
  .of_locallyCompactSpace 𝕜

Похожие утверждения