Bounded monotone sequence theorem (source code)

= Bounded monotone sequence theorem

A real increasing <sequence> bounded above converges to its <supremum>; a decreasing <sequence> bounded below converges to its <infimum>. For the increasing case, the definition of <supremum> provides a term above $L-\varepsilon$, and every later term remains between that term and $L$. Negation reduces the decreasing case to the increasing case. This elementary result is distinct from the measure-theoretic <monotone convergence theorem> for integrals.