Applications of the Hausdorff distance in normed spaces #
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. This is riesz_lemma.
In a nontrivially normed field (with an element c of norm > 1) and any R > ∥c∥, one can
guarantee ∥x∥ ≤ R and ∥x - y∥ ≥ 1 for any y in F. This is riesz_lemma_of_norm_lt.
A further lemma, metric.closed_ball_inf_dist_compl_subset_closure, finds a closed ball within
the closure of a set s of optimal distance from a point in x to the frontier of s.
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.
A version of Riesz lemma: given a strict closed subspace F, one may find an element of norm ≤ R
which is at distance at least 1 of every element of F. Here, R is any given constant
strictly larger than the norm of an element of norm > 1. For a version without an R, see
riesz_lemma.
Since we are considering a general nontrivially normed field, there may be a gap in possible norms
(for instance no element of norm in (1,2)). Hence, we can not allow R arbitrarily close to 1,
and require R > ∥c∥ for some c : 𝕜 with norm > 1.