Topological properties of fixed points

Currently this file contains two lemmas:

• isFixedPt_of_tendsto_iterate: if f^n(x) → y and f is continuous at y, then f y = y;
• isClosed_fixedPoints: the set of fixed points of a continuous map is a closed set.

TODO

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) : Function.IsFixedPt 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) : IsClosed (Function.fixedPoints f)

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