Knaster-Tarski theorem is a simple but powerful fixpoint theorem in order theory. It could give a very elegant proof of Cantor–Bernstein–Schroeder theorem which states that if there are injections and , there exists a bijection between A and B.
Theorem. Let L be a complete lattice and f be a order-preserving morphism from L to L. The sup (join) of the set is the greast fixpoint of f.
Proof. Let . Consider , we have for all , and thus which means that is an upper bound of , i.e. . However, since , we also have which satisfies the predicate of . Hence, and by definition. Finally, we thus have and , so .
The part of greatestness is obvious.
Now, we could simplify the proof of Cantor–Bernstein–Schroeder between sets by explicitly defining the construction of sequence of sets as a function from . However, we also generalise the process than we need.
Theorem. Given two functions and . There are disjoint sets and with and and , .
Proof. Consider which may give a hint that works if it is order-preserving. However, it is obvious that as , . By applying Knaster-Tarski theorem, we have a fixpoint with the desired properties.
Finally, with the help of the above fact we could decompose the domain and codomains of injections and , and thus we have two bijections and where , , , and . Then, define which is obviously bijective. Done.