Theorems · Theorem · functional analysis

LocallyCompactSpace.of_finiteDimensional_of_complete

∀ (K : Type u_4) (V : Type u_5) [inst : NontriviallyNormedField K] [CompleteSpace K] [LocallyCompactSpace K]
  [inst_3 : AddCommGroup V] [inst_4 : TopologicalSpace V] [IsTopologicalAddGroup V] [inst_6 : Module K V]
  [ContinuousSMul K V] [FiniteDimensional K V], LocallyCompactSpace V

If K is a complete field and V is a finite-dimensional vector space over K (equipped with any topology so that V is a topological K-module, meaning [IsTopologicalAddGroup V] and [ContinuousSMul K V]), and K is locally compact, then V is locally compact. This is not an instance because K cannot be inferred.

Defined in

Mathlib.Topology.Algebra.Module.FiniteDimension

Cited by

1 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldCompleteSpaceLocallyCompactSpaceAddCommGroupTopologicalSpaceIsTopologicalAddGroupModuleContinuousSMulFiniteDimensional