English
If a closed ball of positive radius in a normed space is compact, then the space is finite-dimensional.
Русский
Если замкнутый шар положительного радиуса в нормированном пространстве компактен, то пространство конечномерно.
LaTeX
$$$0 < r \\\\Rightarrow IsCompact (Metric.closedBall 0 r) \\\\Rightarrow FiniteDimensional 𝕜 E$$$
Lean4
/-- A locally compact normed vector space is proper. -/
theorem of_locallyCompactSpace (𝕜 : Type*) [NontriviallyNormedField 𝕜] {E : Type*} [SeminormedAddCommGroup E]
[NormedSpace 𝕜 E] [LocallyCompactSpace E] : ProperSpace E :=
by
rcases exists_isCompact_closedBall (0 : E) with ⟨r, rpos, hr⟩
rcases NormedField.exists_one_lt_norm 𝕜 with ⟨c, hc⟩
have hC : ∀ n, IsCompact (closedBall (0 : E) (‖c‖ ^ n * r)) := fun n ↦
by
have : c ^ n ≠ 0 := pow_ne_zero _ <| fun h ↦ by simp [h, zero_le_one.not_gt] at hc
simpa [_root_.smul_closedBall' this] using hr.smul (c ^ n)
have hTop : Tendsto (fun n ↦ ‖c‖ ^ n * r) atTop atTop :=
Tendsto.atTop_mul_const rpos (tendsto_pow_atTop_atTop_of_one_lt hc)
exact .of_seq_closedBall hTop (Eventually.of_forall hC)
