CE_succ
plain-language theorem explainer
The recursive step for the composed extraction operator states that the extractor at level m+1 equals the level-m extractor composed with the local subsequence chosen for column m+1. Analysts building diagonal subsequences for columnwise convergence in bounded double sequences would cite this relation during inductive arguments on the number of columns. The equality holds by direct unfolding of the recursive clause in the definition of the composed extractor.
Claim. Let $CE_m$ be the composed extraction sequence ensuring convergence of columns $0$ through $m$, and let $LE_m$ be the local subsequence selector that forces convergence of column $m+1$ along the image of $CE_m$. Then $CE_{m+1} = CE_m ∘ LE_m$.
background
The module constructs a Cantor diagonal extraction for a bounded double sequence $f:ℕ→ℕ→X$ in a proper metric space, guaranteeing a strictly increasing index map such that every column converges along the extracted subsequence. The composed extraction $CE_m$ is defined recursively: at step 0 it selects a convergent subsequence for column 0; at successor steps it composes the prior extraction with a fresh local subsequence chosen to converge on the next column. The local extraction $LE_m$ is the subsequence selector applied to the image of $CE_m$ that produces convergence at column $m+1$.
proof idea
The proof is a one-line wrapper that applies the recursive clause in the definition of CE at the successor step, which is exactly the stated composition with the local extraction LE.
why it matters
This relation supplies the inductive step for CE_strictMono, CE_factor, CE_conv_le and D_succ_gt. It therefore supports the full diagonal extraction result nat_diagonal_extraction that produces a single strictly increasing map along which every column converges, completing the Fourier-space subsequence extraction without axioms or sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.