Theorems · Theorem · functional analysis

FiniteDimensional.proper

• 1000+ list: Heine–Borel theorem

∀ (𝕜 : Type u) [inst : NontriviallyNormedField 𝕜] (E : Type v) [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [LocallyCompactSpace 𝕜] [FiniteDimensional 𝕜 E], ProperSpace E

Any finite-dimensional vector space over a locally compact field is proper. We do not register this as an instance to avoid an instance loop when trying to prove the properness of 𝕜, and the search for 𝕜 as an unknown metavariable. Declare the instance explicitly when needed.

Defined in

Mathlib.Analysis.Normed.Module.FiniteDimension

Cited by

4 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceLocallyCompactSpaceFiniteDimensional