Editing Knaster–Tarski theorem (section)

==Consequences: least and greatest fixed points==
Since complete lattices cannot be [[empty set|empty]] (they must contain a [[supremum]] and [[infimum]] of the empty set), the theorem in particular guarantees the existence of at least one fixed point of ''f'', and even the existence of a [[least fixed point|''least'' fixed point]] (or [[greatest fixed point|''greatest'' fixed point]]). In many practical cases, this is the most important implication of the theorem.

The [[least fixpoint]] of ''f'' is the least element ''x'' such that ''f''(''x'') = ''x'', or, equivalently, such that ''f''(''x'') ≤ ''x''; the [[duality (order theory)|dual]] holds for the [[greatest fixpoint]], the greatest element ''x'' such that ''f''(''x'') = ''x''.

If ''f''(lim ''x''<sub>''n''</sub>) = lim ''f''(''x''<sub>''n''</sub>) for all ascending [[sequence]]s ''x''<sub>''n''</sub>, then the least fixpoint of ''f'' is lim ''f''<sup>&thinsp;''n''</sup>(0) where 0 is the [[least element]] of ''L'', thus giving a more "constructive" version of the theorem. (See: [[Kleene fixed-point theorem]].) More generally, if ''f'' is monotonic, then the least fixpoint of ''f'' is the stationary limit of ''f''<sup>&thinsp;α</sup>(0), taking α over the [[ordinal number|ordinals]], where ''f''<sup>&thinsp;α</sup> is defined by [[transfinite induction]]: ''f''<sup>&thinsp;α+1</sup> = ''f'' (''f''<sup>&thinsp;α</sup>) and ''f''<sup>&thinsp;γ</sup> for a limit ordinal γ is the [[least upper bound]] of the ''f''<sup>&thinsp;β</sup> for all β ordinals less than γ.<ref>{{cite journal | last1=Cousot | first1=Patrick | last2=Cousot | first2=Radhia | title=Constructive versions of tarski's fixed point theorems | journal=Pacific Journal of Mathematics | year=1979 | volume=82 | pages=43&ndash;57 | doi=10.2140/pjm.1979.82.43| doi-access=free }}</ref> The dual theorem holds for the greatest fixpoint.

For example, in theoretical [[computer science]], least fixed points of [[Monotonic function#In order theory|monotonic function]]s are used to define [[program semantics]], see ''{{seclink|Least fixed point|Denotational semantics}}'' for an example. Often a more specialized version of the theorem is used, where ''L'' is assumed to be the lattice of all subsets of a certain set ordered by [[subset inclusion]]. This reflects the fact that in many applications only such lattices are considered. One then usually is looking for the smallest set that has the property of being a fixed point of the function ''f''. [[Abstract interpretation]] makes ample use of the Knaster–Tarski theorem and the formulas giving the least and greatest fixpoints.

The Knaster–Tarski theorem can be used to give a simple proof of the [[Schröder–Bernstein theorem|Cantor–Bernstein–Schroeder theorem]]<ref>{{MathWorld|author=Uhl, Roland|title=Tarski's Fixed Point Theorem|urlname=TarskisFixedPointTheorem}} Example 3.</ref><ref>{{cite book|last1=Davey|first1=Brian A.|last2=Priestley|first2=Hilary A.|authorlink2=Hilary Priestley|title=Introduction to Lattices and Order|edition=2nd|pages=63, 4|publisher=[[Cambridge University Press]]|year=2002|isbn=9780521784511|title-link= Introduction to Lattices and Order}}</ref> and it is also used in establishing the [[Banach–Tarski paradox]].