Alphabeta Math
DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (z-ai/glm-5.2)audited 2026-07-26
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Nondecreasing, increasing, nonincreasing, decreasing, monotone, and eventually monotone sequences

Definition

Let (xk) be a sequence of reals (Sequences of reals: bounded, eventually, frequently, tails, subsequences), with R ordered as in Order on the reals and Complete ordered field (least-upper-bound property), and with N ordered as in Order on the natural numbers. The sequence is:

  • nondecreasing when xj≤xk for all j≤k;
  • increasing (or strictly increasing) when xj<xk for all j<k;
  • nonincreasing when xj≥xk for all j≤k;
  • decreasing (or strictly decreasing) when xj>xk for all j<k;
  • monotone when it is nondecreasing or nonincreasing;
  • strictly monotone when it is increasing or decreasing;
  • eventually monotone when some tail x(K) (Sequences of reals: bounded, eventually, frequently, tails, subsequences) is monotone, that is when there is K∈N such that the restriction of the comparison to indices ≥K is one-signed.

An increasing sequence is nondecreasing and a decreasing sequence is nonincreasing, since j≤k means j<k or j=k and the second case gives equality. A sequence that is both nondecreasing and nonincreasing is constant.

Consecutive comparisons suffice, and that is an induction. The four conditions above quantify over all pairs of indices, but what one checks in practice, and what a recursive construction delivers, is the comparison of consecutive terms. The two agree:

(xk) is nondecreasing if and only if xk≤xσ(k) for every k∈N, and (xk) is increasing if and only if xk<xσ(k) for every k∈N; likewise, with the inequalities reversed, for nonincreasing and decreasing.

The forward implications are the instances j=k, k=σ(k) of the definitions, using k<σ(k) (Discreteness: σ(n) is the immediate successor). For the converse, suppose xi≤xσ(i) for every i and fix k; we show by induction on k (The principle of mathematical induction) that xj≤xk for every j≤k. For k=0: j≤0 forces j=0, and x0≤x0. Assume the statement for k and let j≤σ(k). If j=σ(k) then xj≤xσ(k) by reflexivity. Otherwise j<σ(k), and then j≤k: were k<j we would have k<j<σ(k), which Discreteness: σ(n) is the immediate successor excludes, so j≤k by totality of the order on N (≤ is a linear order on N). The induction hypothesis gives xj≤xk, and xk≤xσ(k) by assumption, so xj≤xσ(k) by transitivity. This completes the induction. The three remaining equivalences are the same argument with ≤ replaced by <, ≥ or >, transitivity of the strict order being used in the same place.

Boundedness of a monotone sequence is one-sided. A nondecreasing sequence is bounded below by its first term x0, and a nonincreasing sequence is bounded above by x0, both immediately from the definition with j=0. So for a nondecreasing sequence the only substantive question is whether it is bounded above, and for a nonincreasing sequence whether it is bounded below. The range of (xk) is the set {xk:k∈N} (Sequences of reals: bounded, eventually, frequently, tails, subsequences), and it is bounded above, bounded below or bounded in the sense of Lower bound, bounded below, bounded set exactly when the sequence is.

Remarks

  • The naming is the one that keeps "increasing" strict. Some texts use increasing for what is called nondecreasing here and strictly increasing for what is called increasing. This library follows the convention in which the unqualified word is strict, and always writes nondecreasing when equality is allowed, so that no statement on this page depends on which convention a reader arrives with. Where a proof needs the weak form it says nondecreasing, and where it needs the strict form it says increasing.

  • Eventual monotonicity is exactly monotonicity of a tail, and by Convergence depends only on the tail a sequence and its tails converge to the same limits and are Cauchy together. So every convergence statement about monotone sequences on this page extends verbatim to eventually monotone sequences, with the limit unchanged; only statements about specific terms, such as the identification of the limit as the supremum of the whole range, need the hypothesis at every index. The monotone convergence theorem is a case in point: an eventually nondecreasing bounded sequence converges, but to the supremum of the range of the monotone tail, which may be smaller than the supremum of the whole range.

  • Monotone is strictly weaker than strictly monotone, and neither is generic. A constant sequence is monotone and not strictly monotone; the sequence with terms 1 and −1 alternating (The even and odd index maps and the alternating sequence: strictly increasing e,o with N their disjoint union, and the unique (sk) with s0=1, sσ(k)=−sk, which satisfies ∣sk∣=1, s∘e≡1 and s∘o≡−1) is not monotone and not eventually monotone, since every tail contains both values infinitely often. That sequence is bounded, so boundedness alone gives neither form of monotonicity; what it does give is a monotone subsequence (Every real sequence has a monotone subsequence (the peak / rising-sun lemma)), and that is the route to Bolzano-Weierstrass.

Depends on

Used by

…and 4 more results.

Dependency tree · two levels

25 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources