## § Diagonal lemma for monotone functions

- Statement: For a monotone function $f: P \times P \to Q$, we have the equality $f(\sqcup_s s, \sqcup_t t) = f(\sqcup_x (x, x))$
- Since $\sqcup_x (x, x) \sqsubseteq \sqcup_{s, t} (s, t)$, by monotonicity of $f$, we have that $f(\sqcup_x (x, x)) \sqsubseteq f(\sqcup{s, t} (s, t))$.
- On the other hand, note that for each $(s_\star, t_\star)$, we have that $(s_\star, t_\star) \leq \sqcup (s_\star \sqcup t_\star, t_star \sqcup t_\star) = (s_\star, s_star) \sqcup (t_\star, t_\star)$. Thus each element on the RHS is dominated by some element on the LHS.
- So we must have equality of LHS and RHS.

#### § Proving that powering is continuous

- We wish to prove that $f^n$ is continuous, given that $f$ and $(\circ)$ is continuous.
- Proof by induction. $n = 0$ is immediate. For case $n+1$:

$\begin{aligned}
&(\sqcup_f f)^{n+1} \\
&= (\sqcup_f f) \circ (\sqcup_g g)^n \\
&= \sqcup_g ((\sqcup_f f) \circ g^n) \\
&= \sqcup_g \sqcup_f (f \circ g^n) \\
&= \sqcup_f (f \circ f^n) \\
&= \sqcup_f (f^{n+1}) \\
\end{aligned}$

- See that we used the diagonal lemma to convert the union over $f, g$ into a union over $f$.