mathlib documentation


Topological properties of fixed points

Currently this file contains two lemmas:


fixed points, iterates

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

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