---
tag: W46BP9W06H
kind: definition
name: Fixed point
msc: [37C25, 54H25, 37-01]
defines: R6QVS6P21N
uses: [0EPAT51DXQ]
sources:
  - url: https://en.wikipedia.org/wiki/Fixed_point_(mathematics)
---

## Definition

Let $X$ be a set and let $f \colon X \to X$ be a [[map|0EPAT51DXQ]].
A point $x \in X$ is a *fixed point* of $f$ if $f(x) = x$.
The set of fixed points of $f$ is $\operatorname{Fix}(f) = \set{x \in X : f(x) = x}$.

## 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`.