Editing Knaster–Tarski theorem (section)

==Proof==
Let us restate the theorem.

For a complete lattice <math>\langle L, \le \rangle</math> and a monotone function <math>f\colon L \rightarrow L</math> on ''L'', the set of all fixpoints of ''f'' is also a complete lattice <math>\langle P, \le \rangle</math>, with:
* <math>\bigvee P = \bigvee \{ x \in L \mid x \le f(x) \}</math> as the greatest fixpoint of ''f''
* <math>\bigwedge P = \bigwedge \{ x \in L \mid x \ge f(x) \}</math> as the least fixpoint of ''f''.

''Proof.'' We begin by showing that ''P'' has both a least element and a greatest element. Let {{math|1=''D'' = {{mset|''x'' | ''x'' ≤ ''f''(''x'')}}}} and {{math|''x'' ∈ ''D''}} (we know that at least 0<sub>''L''</sub> belongs to ''D''). Then because ''f'' is monotone we have {{math|''f''(''x'') ≤ ''f''(''f''(''x''))}}, that is {{math|''f''(''x'') ∈ ''D''}}.

Now let <math>u = \bigvee D</math> (''u'' exists because {{math|''D'' ⊆ ''L''}} and ''L'' is a complete lattice). Then for all {{math|''x'' ∈ ''D''}} it is true that {{math|''x'' ≤ ''u''}} and {{math|''f''(''x'') ≤ ''f''(''u'')}}, so {{math|''x'' ≤ ''f''(''x'') ≤ ''f''(''u'')}}. Therefore, ''f''(''u'') is an upper bound of ''D'', but ''u'' is the least upper bound, so {{math|''u'' ≤ ''f''(''u'')}}, i.e. {{math|''u'' ∈ ''D''}}. Then {{math|''f''(''u'') ∈ ''D''}} (because {{math|''f''(''u'') ≤ ''f''(''f''(''u'')))}} and so {{math|''f''(''u'') ≤ ''u''}} from which follows ''f''(''u'') = ''u''. Because every fixpoint is in ''D'' we have that ''u'' is the greatest fixpoint of ''f''.

The function ''f'' is monotone on the dual (complete) lattice <math>\langle L^{op}, \ge \rangle</math>. As we have just proved, its greatest fixpoint exists. It is the least fixpoint of ''L'', so ''P'' has least and greatest elements, that is more generally, every monotone function on a complete lattice has a least fixpoint and a greatest fixpoint.

For ''a'', ''b'' in ''L'' we write [''a'', ''b''] for the [[closed interval (order theory)|closed interval]] with bounds ''a'' and {{math|''b'': {{mset|''x'' ∈ ''L'' | ''a'' ≤ ''x'' ≤ ''b''}}}}. If ''a'' ≤ ''b'', then {{angbr|[''a'', ''b''], ≤}} is a complete lattice.

It remains to be proven that ''P'' is a complete lattice. Let <math>1_L = \bigvee L</math>, {{math|''W'' ⊆ ''P''}} and <math>w = \bigvee W</math>. We show that {{math|''f''([''w'', 1<sub>''L''</sub>]) ⊆ [''w'', 1<sub>''L''</sub>]}}. Indeed, for every {{math|''x'' ∈ ''W''}} we have ''x'' = ''f''(''x'') and since ''w'' is the least upper bound of ''W'', {{math|''x'' ≤ ''f''(''w'')}}. In particular {{math|''w'' ≤ ''f''(''w'')}}. Then from {{math|''y'' ∈ [''w'', 1<sub>''L''</sub>]}} follows that {{math|''w'' ≤ ''f''(''w'') ≤ ''f''(''y'')}}, giving {{math|''f''(''y'') ∈ [''w'', 1<sub>''L''</sub>]}} or simply {{math|''f''([''w'', 1<sub>''L''</sub>]) ⊆ [''w'', 1<sub>''L''</sub>]}}. This allows us to look at ''f'' as a function on the complete lattice [''w'', 1<sub>''L''</sub>]. Then it has a least fixpoint there, giving us the least upper bound of ''W''. We've shown that an arbitrary subset of ''P'' has a supremum, that is, ''P'' is a complete lattice.