Theorems · Theorem · functional analysis

FiniteDimensional.of_isCompact_closedBall

∀ (𝕜 : Type u) [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {V : Type u_1} [inst_2 : NormedAddCommGroup V]
  [inst_3 : Module 𝕜 V] [ContinuousSMul 𝕜 V] {r : ℝ},
  0 < r → ∀ {c : V}, IsCompact (Metric.closedBall c r) → FiniteDimensional 𝕜 V

Riesz's theorem: if a closed ball of positive radius is compact in a vector space, then the space is finite-dimensional.

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

NontriviallyNormedFieldCompleteSpaceNormedAddCommGroupModuleContinuousSMul