Theorems · Theorem · functional analysis

NormedSpace.noncompactSpace

∀ (𝕜 : Type u_1) (E : Type u_3) [inst : NormedField 𝕜] [Infinite 𝕜] [inst_2 : NormedAddCommGroup E] [Nontrivial E]
  [NormedSpace 𝕜 E], NoncompactSpace E

A normed vector space over an infinite normed field is a noncompact space. This cannot be an instance because in order to apply it, Lean would have to search for NormedSpace 𝕜 E with unknown 𝕜. We register this as an instance in two cases: 𝕜 = E and 𝕜 = ℝ.

Defined in

Mathlib.Analysis.Normed.Module.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedFieldInfiniteNormedAddCommGroupNontrivialNormedSpace