English
A normed space E over an infinite normed field is noncompact.
Русский
Нормированное пространство E над бесконечным нормированным полем не является компактным.
LaTeX
$$$\\mathrm{NoncompactSpace}(E)$$$
Lean4
/-- 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 `𝕜 = ℝ`. -/
protected theorem noncompactSpace : NoncompactSpace E :=
by
by_cases H : ∃ c : 𝕜, c ≠ 0 ∧ ‖c‖ ≠ 1
· letI := NontriviallyNormedField.ofNormNeOne H
exact ⟨fun h ↦ NormedSpace.unbounded_univ 𝕜 E h.isBounded⟩
· push_neg at H
rcases exists_ne (0 : E) with ⟨x, hx⟩
suffices IsClosedEmbedding (Infinite.natEmbedding 𝕜 · • x) from this.noncompactSpace
refine isClosedEmbedding_of_pairwise_le_dist (norm_pos_iff.2 hx) fun k n hne ↦ ?_
simp only [dist_eq_norm, ← sub_smul, norm_smul]
rw [H, one_mul]
rwa [sub_ne_zero, (Embedding.injective _).ne_iff]
