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

source
theorem riesz_lemma {𝕜 : Type u_1} [NormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Subspace 𝕜 E} (hFc : IsClosed ↑F) (hF : ∃ (x : E), x ∉ F) {r : ℝ} (hr : 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`.

source
theorem riesz_lemma_of_norm_lt {𝕜 : Type u_1} [NormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {c : 𝕜} (hc : 1 < ‖c‖) {R : ℝ} (hR : ‖c‖ < R) {F : Subspace 𝕜 E} (hFc : IsClosed ↑F) (hF : ∃ (x : E), x ∉ F) :
∃ (x₀ : E), ‖x₀‖ ≤ R ∧ ∀ y ∈ F, 1 ≤ ‖x₀ - y‖

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 cannot allow `R` arbitrarily close to `1`, and require `R > ‖c‖` for some `c : 𝕜` with norm `> 1`.

source
theorem Metric.closedBall_infDist_compl_subset_closure {F : Type u_3} [SeminormedAddCommGroup F] [NormedSpace ℝ F] {x : F} {s : Set F} (hx : x ∈ s) :
closedBall x (infDist x s ᶜ) ⊆ closure s