English
For any forward-invariant contracting map f on a complete set S, the edistance between x and the fixed point efixedPoint' is finite whenever hx holds (edist x (f x) ≠ ∞).
Русский
Для любого глобально сжимающего отображения f на полном наборе S расстояние edist между x и фиксированной точкой efixedPoint' конечна при условии hx (edist x (f x) ≠ ∞).
LaTeX
$$$\\operatorname{edist}\\bigl(x, \\mathrm{efixedPoint}'(f,hsc,hsf,hf,x,hxs,hx)\\bigr) < \\infty.$$$
Lean4
theorem edist_efixedPoint_lt_top' {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) ≠ ∞) :
edist x (efixedPoint' f hsc hsf hf x hxs hx) < ∞ :=
(hf.edist_efixedPoint_le' hsc hsf hxs hx).trans_lt
(ENNReal.mul_ne_top hx <| ENNReal.inv_ne_top.2 hf.one_sub_K_ne_zero).lt_top
