偏序集上的单调映射

单调不等于严格单调。严格单调要求 $x{<}_{P}y$ 时 $f(x){<}_{Q}f(y)$；常值映射保持非严格次序，却显然不严格。单调映射也不必反映次序：从任意偏序到单点偏序的映射都是单调的，但它把全部差异压成同一个像。

若 $f$ 既保序又满足

则它反映次序；单射且同时保序、反映次序的映射才是序嵌入。双射的单调映射也未必自动成为序同构，逆映射是否保序仍需检查。

单调性还不同于分析中的连续性。在实数通常次序上，阶跃函数可以单调却在跳点不连续；常值函数连续且单调，但 $x\mapsto x^2$ 在整条实线上连续却不单调。Scott 连续公理库Scott 连续映射Scott-continuous function · Scott continuity保持有向上确界的单调映射，使有限信息逼近与计算相容。要求保存有向上确界，是比单调更强、专门服务信息逼近极限的条件。

幂集上的可达性算子 ​

给定状态集合 $S$、初始集合 $I\subseteq S$ 与一步关系 $\to$，在幂集 $(\mathcal{P}(S),\subseteq )$ 上定义

若 $X\subseteq Y$，每个从 $X$ 中状态出发的一步后继也从 $Y$ 中状态出发，所以 $\mathrm{post}(X)\subseteq \mathrm{post}(Y)$，进而 $F(X)\subseteq F(Y)$。这是一份完整的单调性证明：先任取较小集合中的像元素，再用包含关系把同一个见证搬到较大集合。

从 $X_0=\varnothing$ 开始迭代，得到

每一步都不小于前一步，有限状态空间中最终会稳定在全部可达状态。这里的增长来自 $F$ 的具体形式与初值；“$F$ 单调”本身并不保证任意轨道 $x,F(x),F^2(x),\dots$ 都递增，还需先有 $x\le F(x)$。

组合、点态次序与反例 ​

单调映射的复合仍单调。若 $f:P\to Q$、$g:Q\to R$ 都保序，则 $x{\le }_{P}y$ 依次推出 $f(x){\le }_{Q}f(y)$ 与 $g(f(x)){\le }_{R}g(f(y))$。这使复杂转移函数可以由局部保序部件组合，而无需重新逐点证明整体方向。

函数集合 $Q^P$ 若按点态次序

排序，就能比较两个分析器或变换器谁给出的结果更小。点态比较不是按函数值总和、运行时间或语法长度排序，量词覆盖定义域中的每个输入。

一个常见失败是把“对若干样本保持大小”当作全称证明。例如 $h(x)=x^2$ 在 $0,1,2$ 上递增，却在 $-2<-1$ 时给出 $4>1$，因此不是 $\mathbb{R}$ 上的单调映射。另一种错误是把 antitone 映射也叫单调：集合补运算满足 $A\subseteq B\Rightarrow B^c\subseteq A^c$，它反转而非保持次序。

单调算子把“输入信息增加时，结论不能倒退”形式化，是完备格公理库完备格Complete lattice · Complete ordered lattice任意子集都具有上确界和下确界，从而包含顶元、底元并支持任意族合流的格。、数据流方程和抽象语义的共同接口。Knaster–Tarski 不动点定理只要求完备格上的单调自映射，不要求距离、导数或压缩常数。

这也说明单调与收敛速度是两件事。单调性允许按次序比较迭代结果，却不承诺有限步稳定，更不承诺唯一不动点；在无限升链上，迭代可能持续增长，静态分析因而还需要 widening 等终止机制。