isFixedPt_of_tendsto_iterate — Mathlib

English

If the iterates f^[n] x converge to y and f is continuous at y, then y is a fixed point of f.

Русский

Если последовательность итераций f^[n] x сходится к y и f непрерывна в точке y, то y является фиксированной точкой f.

LaTeX

$$$\text{Tendsto} (n \mapsto f^{[n]}(x))_{n\to\infty} \to \mathcal{N}(y) \; \&\; \text{ContinuousAt } f\ y \Rightarrow IsFixedPt f y$$$

Lean4

/-- If the iterates `f^[n] x` converge to `y` and `f` is continuous at `y`,
then `y` is a fixed point for `f`. -/
theorem isFixedPt_of_tendsto_iterate {x y : α} (hy : Tendsto (fun n => f^[n] x) atTop (𝓝 y)) (hf : ContinuousAt f y) :
    IsFixedPt f y := by
  refine tendsto_nhds_unique ((tendsto_add_atTop_iff_nat 1).1 ?_) hy
  simp only [iterate_succ' f]
  exact hf.tendsto.comp hy

Похожие утверждения