Topological properties of fixed points #

Currently this file contains two lemmas:


fixed points, iterates

theorem isFixedPt_of_tendsto_iterate {α : Type u_1} [TopologicalSpace α] [T2Space α] {f : αα} {x : α} {y : α} (hy : Filter.Tendsto (fun (n : ) => f^[n] x) Filter.atTop (nhds y)) (hf : ContinuousAt 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 isClosed_fixedPoints {α : Type u_1} [TopologicalSpace α] [T2Space α] {f : αα} (hf : Continuous f) :

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