Diagonal subsequence argument (source code)

= Diagonal subsequence argument

A diagonal subsequence argument successively extracts nested subsequences that converge in the first, first two, and then first $k$ coordinates. Taking the $j$th term from the $j$th nested subsequence produces one subsequence that converges in every fixed coordinate.