Topological properties of fixed points
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 : α} :
filter.tendsto (λ (n : ℕ), f^[n] x) filter.at_top (nhds y) → continuous_at f y → function.is_fixed_pt 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 : α → α} :
continuous f → is_closed (function.fixed_points f)
The set of fixed points of a continuous map is a closed set.