# mathlibdocumentation

dynamics.fixed_points.topology

# Topological properties of fixed points #

Currently this file contains two lemmas:

• is_fixed_pt_of_tendsto_iterate: if f^n(x) → y and f is continuous at y, then f y = y;
• is_closed_fixed_points: the set of fixed points of a continuous map is a closed set.

## TODO #

fixed points, iterates

theorem is_fixed_pt_of_tendsto_iterate {α : Type u_1} [t2_space α] {f : α → α} {x y : α} (hy : filter.tendsto (λ (n : ), f^[n] x) filter.at_top (𝓝 y)) (hf : 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} [t2_space α] {f : α → α} (hf : continuous f) :

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