完全格中的最小不动点与单调映射：证明G₁的单调性
我来帮你梳理这个证明的关键步骤，核心就是利用单调映射的最小不动点关于参数的单调性这个性质，咱们一步步拆解：
先明确已知条件
- 给定两个完全格 $(E_1,\leq_1)$ 和 $(E_2,\leq_2)$
- 映射 $f_1: E_1 \times E_2 \to E_1$ 和 $f_2: E_1 \times E_2 \to E_2$ 关于两个变量都是单调的（即任意一个变量增大时，映射结果不减小）
- 对固定的 $Y \in E_1$，定义 $F_2^Y(Z) = f_2(Y,Z)$，它是单调映射，根据Knaster-Tarski引理，其最小不动点 $\mu F_2^Y$ 存在且唯一
- 目标是证明 $G_1(Y) = f_1(Y, \mu F_2^Y)$ 关于 $Y$ 是单调的，即：若 $Y \leq_1 Y'$，则 $G_1(Y) \leq_1 G_1(Y')$
关键步骤：证明 $\mu F_2^Y \leq_2 \mu F_2^{Y'}$
这是整个证明的核心，我们可以通过Knaster-Tarski引理的前不动点性质来推导：
因为 $Y \leq_1 Y'$，且 $f_2$ 关于第一个变量单调，所以对任意 $Z \in E_2$，有：
$$f_2(Y,Z) \leq_2 f_2(Y',Z)$$
也就是 $F_2^Y(Z) \leq_2 F_2^{Y'}(Z)$ 对所有 $Z$ 成立。我们知道 $\mu F_2^{Y'}$ 是 $F_2^{Y'}$ 的不动点，即：
$$F_2^{Y'}(\mu F_2^{Y'}) = \mu F_2^{Y'}$$结合第一步的单调性，代入 $Z = \mu F_2^{Y'}$ 可得：
$$F_2^Y(\mu F_2^{Y'}) \leq_2 F_2^{Y'}(\mu F_2^{Y'}) = \mu F_2^{Y'}$$
这说明 $\mu F_2^{Y'}$ 是 $F_2^Y$ 的前不动点（满足 $F_2^Y(W) \leq_2 W$ 的元素）。根据Knaster-Tarski引理，最小不动点 $\mu F_2^Y$ 是 $F_2^Y$ 的所有前不动点的下确界，同时也是最小的前不动点。因此对任意前不动点 $W$，都有 $\mu F_2^Y \leq_2 W$。
这里 $\mu F_2^{Y'}$ 就是 $F_2^Y$ 的一个前不动点，所以必然有：
$$\mu F_2^Y \leq_2 \mu F_2^{Y'}$$
最终证明 $G_1$ 的单调性
现在我们已经得到 $\mu F_2^Y \leq_2 \mu F_2^{Y'}$，结合 $f_1$ 的单调性：
- 因为 $Y \leq_1 Y'$，且 $f_1$ 关于第一个变量单调，所以 $f_1(Y, \mu F_2^Y) \leq_1 f_1(Y', \mu F_2^Y)$
- 又因为 $\mu F_2^Y \leq_2 \mu F_2^{Y'}$，且 $f_1$ 关于第二个变量单调，所以 $f_1(Y', \mu F_2^Y) \leq_1 f_1(Y', \mu F_2^{Y'})$
把这两个不等式连起来，就得到：
$$G_1(Y) = f_1(Y, \mu F_2^Y) \leq_1 f_1(Y', \mu F_2^{Y'}) = G_1(Y')$$
补充：针对有限幂集格的验证
你提到关注的是有限幂集格（包含关系为序），这个证明依然完全适用。另外在有限格中，最小不动点可以通过从底元素（空集）迭代计算得到：
- 从 $Z_0 = \emptyset$ 开始，迭代 $Z_{n+1} = F_2^Y(Z_n)$，$Z'_{n+1} = F_2^{Y'}(Z_n)$
- 由于 $F_2^Y(Z_n) \subseteq F_2^{Y'}(Z_n)$ 对每一步成立，最终迭代到不动点时，必然有 $\mu F_2^Y \subseteq \mu F_2^{Y'}$，这也能直观验证我们的结论。
备注：内容来源于stack exchange，提问作者deopen
