tendsto_comp_strictMono
plain-language theorem explainer
If a sequence f from naturals to a topological space converges to x at infinity, then its reindexing along any strictly increasing map ψ also converges to x. Analysts building diagonal extractions or Fourier subsequence arguments in Navier-Stokes settings cite this to preserve limits under monotone reindexing. The proof is a one-line wrapper that composes the given tendsto hypothesis with the tendsto_atTop property of strict monotonicity.
Claim. Let $X$ be a topological space. Suppose the sequence $f : ℕ → X$ satisfies $f(n) → x$ as $n → ∞$. If $ψ : ℕ → ℕ$ is strictly increasing, then $f(ψ(n)) → x$ as $n → ∞$.
background
The module develops Fourier-space subsequential extraction by Cantor diagonal methods for bounded sequences in proper metric spaces, with every result fully proved. This theorem records the elementary fact that convergence at infinity is stable under strictly monotone reindexing, a step needed to construct the CE and CL objects that extract pointwise convergent subsequences. Upstream composition definitions in cost algebras, arithmetic homomorphisms, octave morphisms, and vantage functors establish how maps are combined while preserving multiplicative structure, order, and strain in the surrounding Recognition framework.
proof idea
The proof is a one-line wrapper that applies the composition rule for tendsto maps to the hypothesis hf together with the fact that any strict mono ψ satisfies ψ.tendsto_atTop.
why it matters
The declaration supplies the reindexing preservation step required by the downstream CE_conv_le theorem, which proves pointwise convergence of the extracted sequences to the CL limit. It fits inside the module's diagonal extraction pipeline and inherits the order-preservation properties built into the octave and vantage composition operations. No open scaffolding remains; the result closes a standard analytic prerequisite for the fully proved extraction claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.