Theorems · Theorem · functional analysis

riesz_lemma

∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  {F : Subspace 𝕜 E}, IsClosed ↑F → (∃ x, x ∉ F) → ∀ {r : ℝ}, r < 1 → ∃ x₀ ∉ F, ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖

Riesz's lemma, which usually states that it is possible to find a vector with norm 1 whose distance to a closed proper subspace is arbitrarily close to 1. The statement here is in terms of multiples of norms, since in general the existence of an element of norm exactly 1 is not guaranteed. For a variant giving an element with norm in [1, R], see riesz_lemma_of_norm_lt, and for a variant giving an element with norm exactly one assuming stronger assumptions on the underlying field, see riesz_lemma_of_lt_one.

Defined in

Mathlib.Analysis.Normed.Module.RieszLemma

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedFieldNormedAddCommGroupNormedSpace