isClosed_fixedPoints
theorem isClosed_fixedPoints :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : T2Space α] {f : α → α},
Continuous f → IsClosed (Function.fixedPoints f)
This theorem states that for any type `α` that is equipped with a topological space structure and a T2 space (also known as a Hausdorff space) structure, the set of fixed points for any continuous function `f` (a function from `α` to `α`) is a closed set. In mathematical terms, given a continuous function `f: α → α` in a Hausdorff space, the set of all elements `x` such that `f(x) = x` forms a closed set.
More concisely: In a Hausdorff space endowed with a topology and a continuous function, the fixed point set of the function is a closed set.
|
isFixedPt_of_tendsto_iterate
theorem isFixedPt_of_tendsto_iterate :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : T2Space α] {f : α → α} {x y : α},
Filter.Tendsto (fun n => f^[n] x) Filter.atTop (nhds y) → ContinuousAt f y → Function.IsFixedPt f y
This theorem states that for a given function `f` from a topological space `α`, if the iterates of `f` at a point `x` (represented as `f^[n] x`) converge to a point `y` (in the sense that as `n` tends to infinity, `f^[n] x` gets arbitrarily close to `y`), and if `f` is continuous at `y`, then `y` is a fixed point for `f` (i.e., `f(y) = y`). This is under the assumption that the topological space `α` is a `T2` space (also known as a Hausdorff space), which is a topological space where any two distinct points have disjoint open neighborhoods.
More concisely: If a continuous function `f` from a T2 topological space `α` has a point `x` such that the iterates `f^[n] x` converge to a point `y`, then `y` is a fixed point of `f` (i.e., `f(y) = y`).
|