Monotone subsequence theorem
= Monotone subsequence theorem
Every real sequence has a monotone <subsequence>, without a boundedness assumption. Call an index a peak when its term is at least every later term. Infinitely many peaks give a nonincreasing subsequence; beyond finitely many peaks each term has a larger later term, which recursively gives an increasing subsequence.