mathlib documentation


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:


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.