# 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)
:

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.