Alphabeta Math
DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (z-ai/glm-5.2)audited 2026-07-28
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 (strictly increasing), nonincreasing, decreasing, monotone and strictly monotone real functions on a subset of R, with the dictionary to monotone sequences

Definition

Throughout, R is the complete ordered field (Complete ordered field (least-upper-bound property), Ordered field) with its order (Order on the reals). Let A⊆R and let f:A→R. Then f is:

  • nondecreasing when f(x)≤f(y) for all x,y∈A with x≤y;
  • increasing, or strictly increasing, when f(x)<f(y) for all x,y∈A with x<y;
  • nonincreasing when f(x)≥f(y) for all x,y∈A with x≤y;
  • decreasing, or strictly decreasing, when f(x)>f(y) for all x,y∈A with x<y;
  • monotone when it is nondecreasing or nonincreasing;
  • strictly monotone when it is increasing or decreasing.

The naming follows the convention of Nondecreasing, increasing, nonincreasing, decreasing, monotone, and eventually monotone sequences, which is the convention of this library throughout: increasing is the strict notion and nondecreasing the weak one.

An increasing function is nondecreasing, and a decreasing function is nonincreasing. For x≤y either x<y, and then f(x)<f(y), hence f(x)≤f(y); or x=y, and then f(x)=f(y). The same argument with the inequalities reversed gives the second claim. So strictly monotone implies monotone.

A strictly monotone function is injective (Injection, surjection, bijection). Let f be increasing and let x,y∈A with x≠y. By trichotomy either x<y, and then f(x)<f(y), or y<x, and then f(y)<f(x); in both cases f(x)≠f(y). The decreasing case is the same argument. The converse fails, and the failure is not exotic: a continuous injection on an interval is strictly monotone (A continuous injective function on an interval is strictly monotone), but on a domain that is not an interval it need not be.

Negation exchanges the two directions. For g:=−f, that is g(x):=−f(x), the four conditions above are exchanged in pairs: f is nondecreasing exactly when g is nonincreasing, and f is increasing exactly when g is decreasing, because u≤v holds exactly when −v≤−u (Ordered field). Several proofs below use this to reduce a nonincreasing case to a nondecreasing one.

Monotone on a set, not at a point. All six conditions are conditions on the whole of A; unlike continuity (Continuity of f:A→R at a point of A and on A: the ε-δ condition, its agreement with lim⁡x→cf(x)=f(c) at a limit point, and continuity at an isolated point) there is no pointwise version, and none is used in this library. The domain A is an arbitrary subset of R; where a result needs A to be an interval (Intervals of R: the nine order-convex forms, nondegeneracy, and length) it says so, and the hypothesis is never decoration.

The dictionary to monotone sequences

A sequence of reals is a function x:N→R (Sequences of reals: bounded, eventually, frequently, tails, subsequences), and Nondecreasing, increasing, nonincreasing, decreasing, monotone, and eventually monotone sequences calls it nondecreasing when xj≤xk for all j≤k, increasing when xj<xk for all j<k, and so on. Those are the same four conditions as above, read with the ordered set N in place of the ordered subset A⊆R and with the comparison of indices in place of the comparison of arguments. So nothing new is introduced here for sequences, and the two vocabularies may be used interchangeably: the words nondecreasing, increasing, nonincreasing, decreasing, monotone and strictly monotone mean the corresponding condition on the domain at hand.

One consequence is used repeatedly, and it has to be stated carefully because composition does not simply preserve the four words. Let (xk) be a nondecreasing sequence with xk∈A for every k, so that j≤k gives xj≤xk. Then:

  • if f is nondecreasing, (f(xk)) is nondecreasing, since f(xj)≤f(xk);
  • if f is nonincreasing, (f(xk)) is nonincreasing, since f(xj)≥f(xk).

So along a nondecreasing sequence the composite inherits the direction of f; and with (xk) increasing and f increasing, (f(xk)) is increasing, while with (xk) increasing and f decreasing, (f(xk)) is decreasing.

Along a nonincreasing sequence the direction is reversed, not inherited. If (xk) is nonincreasing and f is nonincreasing, then j≤k gives xj≥xk and hence f(xj)≤f(xk): the composite is nondecreasing. The witness is f(x)=−x on A=R with xk=−k, where both f and (xk) are decreasing and f(xk)=k is increasing. Two order-reversing maps compose to an order-preserving one, exactly as for the four words applied to functions.

Depends on

Used by

…and 9 more results.

Dependency tree · two levels

20 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