Riesz's lemma relative to a larger subspace #
Mathlib's riesz_lemma_of_norm_lt finds, outside a proper closed subspace F of a normed space,
a vector of controlled norm at distance at least 1 from F. This file records the relative
form: when F is a proper closed subspace of a subspace G, the vector can be chosen in G.
This is the form used to build separated sequences along strictly decreasing chains of closed
subspaces, as in the Riesz theory of compact operators.
theorem
TauCeti.riesz_lemma_of_norm_lt_of_lt
{𝕜 : Type u_1}
{E : Type u_2}
[NormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{c : 𝕜}
(hc : 1 < ‖c‖)
{R : ℝ}
(hR : ‖c‖ < R)
{F G : Submodule 𝕜 E}
(hFc : IsClosed ↑F)
(hFG : F < G)
:
Riesz's lemma relative to a larger subspace: if F is a closed subspace properly contained
in a subspace G, then G contains a vector of norm at most R at distance at least 1
from F.