Least fixed point

Remarks

A least fixed point is unique when it exists, by antisymmetry of $\le$. It is written $\operatorname{lfp}(f)$ or $\mu f$. The greatest fixed point is defined dually and written $\operatorname{gfp}(f)$ or $\nu f$. Example: for $f \colon \R \to \R$, $f(x) = x^2$, the fixed points are the solutions of $x^2 = x$, namely $0$ and $1$. Since $0 \le 1$, the least fixed point is $0$. Non-example: for $g \colon \R \to \R$, $g(x) = x$, every real number is a fixed point, and $\R$ has no least element, so $g$ has no least fixed point. The map $x \mapsto x + 1$ on $\R$ has no fixed point at all.