mathlib documentation

dynamics.fixed_points.topology

Topological properties of fixed points

Currently this file contains two lemmas:

TODO

fixed points, iterates

theorem is_fixed_pt_of_tendsto_iterate {α : Type u_1} [topological_space α] [t2_space α] {f : α → α} {x y : α} :

If the iterates f^[n] x converge to y and f is continuous at y, then y is a fixed point for f.

theorem is_closed_fixed_points {α : Type u_1} [topological_space α] [t2_space α] {f : α → α} :

The set of fixed points of a continuous map is a closed set.