Riesz's lemma
Riesz's lemma, stated for a normed space over a normed field: for any closed proper subspace F of E, there is a nonzero x such that ∥x - F∥ is at least r * ∥x∥ for any r < 1.
theorem
riesz_lemma
{𝕜 : Type u_1}
[normed_field 𝕜]
{E : Type u_2}
[normed_group E]
[normed_space 𝕜 E]
{F : subspace 𝕜 E}
(hFc : is_closed ↑F)
(hF : ∃ (x : E), x ∉ F)
{r : ℝ}
(hr : r < 1) :
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.