LE
plain-language theorem explainer
The local extraction at level m selects a strictly increasing index map for the (m+1)th column after the prior composed extraction up to m has been applied. Analysts constructing diagonal subsequences in proper metric spaces cite this incremental step to ensure column-wise convergence. The definition is a one-line wrapper that applies the bounded subsequence extraction theorem to the precomposed column sequence and extracts the witness map.
Claim. Let $f : ℕ → ℕ → X$ be a double sequence bounded in the closed ball of radius $R$ around $c$ in a proper metric space $X$. For each $m$, the map $λ_m : ℕ → ℕ$ is the strictly monotone index selector such that $f(λ_m(n), m+1)$ converges, obtained by applying subsequence extraction to the sequence $n ↦ f(φ_m(n), m+1)$ where $φ_m$ is the composed extraction up to column $m$.
background
The module implements Cantor diagonal extraction so that a single subsequence makes every column of a double-indexed sequence converge in a proper metric space. The upstream theorem bounded_subseq_tendsto states that any sequence bounded in a closed ball admits a convergent subsequence extracted by a strictly monotone index map. CE is the recursive composed extraction ensuring the first $m$ columns converge simultaneously. LE supplies the incremental index map needed for column $m+1$.
proof idea
This is a one-line wrapper that applies bounded_subseq_tendsto to the sequence fun n => f (CE m n) (m+1) together with the restricted boundedness hypothesis. The .choose operator extracts the witness strictly increasing map.
why it matters
LE is used to establish CE_succ, which shows the extraction at step $m+1$ equals the prior extraction composed with this local map. The step closes the inductive construction for the main result nat_diagonal_extraction guaranteeing one subsequence along which all columns converge. In the Recognition framework it supplies the extraction mechanism that supports deriving continuous structures such as reals and time from discrete logic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.