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:
is_fixed_pt_of_tendsto_iterate: iff^n(x) → yandfis continuous aty, thenf 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}
[topological_space α]
[t2_space α]
{f : α → α}
{x y : α}
(hy : filter.tendsto (λ (n : ℕ), f^[n] x) filter.at_top (nhds 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.