# 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.closedBall_infDist_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`

.