equal
deleted
inserted
replaced
13 subsection {* Prose version *}; |
13 subsection {* Prose version *}; |
14 |
14 |
15 text {* |
15 text {* |
16 According to the book ``Introduction to Lattices and Order'' |
16 According to the book ``Introduction to Lattices and Order'' |
17 \cite[pages 93--94]{davey-priestley}, the Knaster-Tarski fixpoint |
17 \cite[pages 93--94]{davey-priestley}, the Knaster-Tarski fixpoint |
18 theorem is as follows.\footnote{We have dualized their argument, and |
18 theorem is as follows.\footnote{We have dualized the argument, and |
19 tuned the notation a little bit.} |
19 tuned the notation a little bit.} |
20 |
20 |
21 \medskip \textbf{The Knaster-Tarski Fixpoint Theorem.} Let $L$ be a |
21 \medskip \textbf{The Knaster-Tarski Fixpoint Theorem.} Let $L$ be a |
22 complete lattice and $f \colon L \to L$ an order-preserving map. |
22 complete lattice and $f \colon L \to L$ an order-preserving map. |
23 Then $\bigwedge \{ x \in L \mid f(x) \le x \}$ is a fixpoint of $f$. |
23 Then $\bigwedge \{ x \in L \mid f(x) \le x \}$ is a fixpoint of $f$. |