Theorems · Theorem · functional analysis

exists_norm_le_le_norm_sub_of_finset

∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type v} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [CompleteSpace 𝕜] {c : 𝕜},
  1 < ‖c‖ → ∀ {R : ℝ}, ‖c‖ < R → ¬FiniteDimensional 𝕜 E → ∀ (s : Finset E), ∃ x, ‖x‖ ≤ R ∧ ∀ y ∈ s, 1 ≤ ‖y - x‖

In an infinite-dimensional space, given a finite number of points, one may find a point with norm at most R which is at distance at least 1 of all these points.

Defined in

Mathlib.Analysis.Normed.Module.FiniteDimension

Cited by

1 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceCompleteSpace