Topological properties of fixed points #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
Currently this file contains two lemmas:
fixed points, iterates
If the iterates
f^[n] x converge to
f is continuous at
y is a fixed point for
The set of fixed points of a continuous map is a closed set.