Fixed point

Remarks

If $x$ is a fixed point of $f$, then $f^n(x) = x$ for every $n \ge 0$, so the orbit of $x$ is the single point $\set{x}$.

Example: $f(x) = \cos x$ on $\R$ has a fixed point $x_0 \in (0, 1)$. Indeed $g(x) = \cos x - x$ is continuous with $g(0) = 1 > 0$ and $g(1) = \cos 1 - 1 < 0$, so $g$ vanishes somewhere in $(0, 1)$.

Non-example: the translation $f(x) = x + 1$ on $\R$ has no fixed point, since $x + 1 \ne x$ for every $x$.

For a function of one real variable, $x$ is a fixed point exactly when the graph of $f$ meets the line $y = x$ at $(x, x)$. In Lean's Mathlib the predicate is Function.IsFixedPt f x.