偏序集上的单调映射

单调不等于严格单调。严格单调要求 $x{<}_{P}y$ 时 $f(x){<}_{Q}f(y)$；常值映射保持非严格次序；当定义域中存在 $x{<}_{P}y$ 时，它不严格单调。若定义域是反链，严格单调条件没有可检验的不同可比元素，连常值映射也会真空地满足该条件。单调映射也不必反映次序：从任意偏序到单点偏序的映射都是单调的，但它把全部差异压成同一个像。

若 $f$ 既保序又满足

则它反映次序；同时保序、反映次序的映射称为序嵌入。反映次序已经保证单射：若 $f(x)=f(y)$，便同时推出 $x{\le }_{P}y$ 与 $y{\le }_{P}x$，由反对称性得 $x=y$。双射的单调映射未必是序同构：把两元素反链双射到两元素链时，定义域没有不同元素之间的比较，保序条件自动成立；逆映射却把链中的比较送到不可比元素上，因而不保序。

单调性还不同于分析中的连续性。在实数通常次序上，阶跃函数可以单调却在跳点不连续；常值函数连续且单调，但 $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 等终止机制。

点态次序也可以认证连续变形 ​

对有限偏序，把全部严格比较链组成序复形理路有限偏序的序复形与同伦证书Order complex and order homotopy · Finite poset homotopy certificate · 序复形把有限偏序的全部比较链变成单纯复形，用逐点保序更新和可删除点日志交付连续同伦与链证书。。本页的点态比较 $f\le g$ 于是有拓扑含义：从差异源点中的极大点开始逐个改值，至多 $|P|$ 步得到同伦，每一步的像顶点都位于同一目标单形。菱形例中的 $(0,a)\to (0,1)\to (b,1)$ 表明，端点逐点可比虽够构造同伦，却未必够一次直接的单形内插值。

偏序纤维引理理路Quillen有限偏序纤维引理Quillen poset fiber lemma · McCord–Quillen theorem · Quillen Theorem A for finite posets由每个下理想原像的可缩性认证指定序复形映射是同伦等价，并通过有限映射柱的两份删点序列证明结论。进一步把指定保序映射是否给同伦等价转为全部下理想原像的可缩性。它检查 $\{x:f(x)\le y\}$，不是仅查 $f^{-1}(y)$；本页两点反链到两点链的保序双射正好见证后者不够。