Theorems · Theorem · functional analysis

ProperSpace.of_locallyCompact_module

∀ (𝕜 : Type u) [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] (V : Type u_1) [inst_2 : AddCommGroup V]
  [inst_3 : TopologicalSpace V] [IsTopologicalAddGroup V] [T2Space V] [Nontrivial V] [LocallyCompactSpace V]
  [inst_8 : Module 𝕜 V] [ContinuousSMul 𝕜 V], ProperSpace 𝕜

Defined in

Mathlib.Analysis.Normed.Module.FiniteDimension

Cited by

1 results in Mathlib

Foundations

Depth 176 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldCompleteSpaceAddCommGroupTopologicalSpaceIsTopologicalAddGroupT2SpaceNontrivialLocallyCompactSpaceModuleContinuousSMul