limit_in_closedBall
plain-language theorem explainer
In a pseudo-metric space the limit of any sequence contained in a closed ball of radius R around c remains inside that ball. PDE analysts working with Galerkin approximations for Navier-Stokes cite the fact when passing to limits inside bounded sets of function space. The proof is a one-line wrapper that invokes le_of_tendsto on the distance function together with the constant-sequence filter and the eventual-forall property.
Claim. Let $(X,d)$ be a pseudo-metric space, let $f:ℕ→X$ be a sequence, let $c∈X$ and $R∈ℝ$. If $d(f(n),c)≤R$ for every $n$ and $f$ converges to some $x∈X$, then $d(x,c)≤R$.
background
The declaration sits inside the GalerkinEquicontinuity module whose module doc describes Lipschitz constants for Fourier coefficients, rational approximation, and the McShane upper extension $g(t)=inf_{q∈ℚ}(g_rat(q)+L|t-q|)$ that produces an L-Lipschitz dense extension. The local theoretical setting is the construction of equicontinuous families needed for 3-D Navier-Stokes Galerkin schemes. Upstream results supply structural facts such as the ledger L (debit and credit both constantly 1), the CirclePhaseLift.and theorem that produces an explicit angular Lipschitz constant $M r$, and various is theorems that certify algebraic or combinatorial consistency without new axioms.
proof idea
The proof is a one-line wrapper that applies le_of_tendsto to the continuous map $y↦d(y,c)$ along the sequence $f$. It uses the fact that the constant sequence at $c$ converges in the filter sense and that the inequality $d(f(n),c)≤R$ holds for all $n$, hence eventually.
why it matters
The result supplies the closedness of closed balls required to keep limit points inside the bounded sets that appear in the McShane extension step of the Galerkin equicontinuity argument. It therefore supports the overall equicontinuity machinery for Navier-Stokes approximations inside the Recognition monolith. No direct downstream use is recorded in the current graph, and the statement does not invoke the phi-ladder or T5–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.