of_isCompact_closedBall — Mathlib

English

Any finite-dimensional normed real vector space E is a proper space.

Русский

Любое конечномерное нормированное вещественное пространство E является правильным (proper).

LaTeX

$$$[FiniteDimensional 𝕜 E] \\\\Rightarrow \\text{ProperSpace } E$$$

Lean4

/-- **Riesz's theorem**: if a closed ball of positive radius is compact in a vector space, then the
space is finite-dimensional. -/
theorem of_isCompact_closedBall {r : ℝ} (rpos : 0 < r) {c : E} (h : IsCompact (Metric.closedBall c r)) :
    FiniteDimensional 𝕜 E :=
  .of_isCompact_closedBall₀ 𝕜 rpos <| by simpa using h.vadd (-c)

Похожие утверждения