D_strictMono
plain-language theorem explainer
The diagonal map D(n) = CE(f, c, R, hf)(n, n) is strictly increasing on the naturals. Analysts constructing subsequence extractions for bounded sequences in proper metric spaces cite this to guarantee a strictly monotone index selector φ. The proof is a one-line wrapper that feeds the successor inequalities from D_succ_gt into strictMono_nat_of_lt_succ.
Claim. Let $D(n) := CE(f,c,R,hf)(n,n)$. Then $D$ is strictly monotone: $n < m$ implies $D(n) < D(m)$.
background
In the Fourier-Space Subsequential Extraction module the double sequence CE produces terms in a proper metric space X. The auxiliary definition D extracts the main diagonal by setting D(n) to CE(f,c,R,hf)(n,n). The upstream lemma D_succ_gt proves D(n) < D(n+1) by rewriting via CE_succ and invoking CE_strictMono on the second argument after the natural-number ordering lt_of_lt_of_le (Nat.lt_succ_of_le le_rfl).
proof idea
The proof is a one-line wrapper that applies strictMono_nat_of_lt_succ to the successor family supplied by D_succ_gt.
why it matters
D_strictMono supplies the StrictMono φ clause inside the main Cantor diagonal extraction theorem nat_diagonal_extraction. That theorem assembles a strictly increasing index map together with a pointwise limit function g, furnishing the subsequential limits required for Fourier-space analysis of the Navier-Stokes equations. The result is fully proved with no open scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.