instProperSpaceSubtypeMemSubmoduleOfCompleteSpaceOfLocallyCompactSpace

English

A submodule of a locally compact complete field space is locally compact and proper.

Русский

Подмодуль локально компактного пространства над полем является локально компактным и правильным.

LaTeX

$$$\\text{ProperSpace S}$ for S a Submodule in locally compact space$$

Lean4

/-- A submodule of a locally compact space over a complete field is also locally compact (and even
proper). -/
instance {𝕜 E : Type*} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E]
    [LocallyCompactSpace E] (S : Submodule 𝕜 E) : ProperSpace S :=
  by
  nontriviality E
  have : ProperSpace 𝕜 := .of_locallyCompact_module 𝕜 E
  have : FiniteDimensional 𝕜 E := .of_locallyCompactSpace 𝕜
  exact FiniteDimensional.proper 𝕜 S

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