English
Let S be a complete forward-invariant subset of a metric space X, and let f: X → X map S into S with contraction constant K < 1 on S. If x ∈ S and edist(x, f(x)) is finite, then the iterates f^[n](x) converge to the distinguished fixed point of f on S determined by x.
Русский
Пусть S — полное впередInvariant подмножество метрического пространства X, и пусть f: X → X отправляет S в S, удовлетворяя условию сжатия с константой K < 1 на S. Если x ∈ S и edist(x, f(x)) конечна, то итерации f^[n](x) сходятся к определённой фиксированной точке f на S, полученной из x.
LaTeX
$$$\\displaystyle \\text{Tendsto}\\bigl(n \\mapsto f^{[n]}(x)\\bigr)_{n \\to \\infty} = \\mathrm{efixedPoint}'(f,hsc,hsf,hf,x,hxs,hx).$$$
Lean4
theorem tendsto_iterate_efixedPoint' {s : Set α} (hsc : IsComplete s) (hsf : MapsTo f s s)
(hf : ContractingWith K <| hsf.restrict f s s) {x : α} (hxs : x ∈ s) (hx : edist x (f x) ≠ ∞) :
Tendsto (fun n ↦ f^[n] x) atTop (𝓝 <| efixedPoint' f hsc hsf hf x hxs hx) :=
(Classical.choose_spec <| hf.exists_fixedPoint' hsc hsf hxs hx).2.2.1
