English
If the distance between x and y is finite, then efixedPoint' from x on S equals efixedPoint' from y on T, under contracting conditions.
Русский
Если расстояние между x и y конечно, то фиксированные точки из x и из y совпадают при условиях сжатия на S и T.
LaTeX
$$$\\operatorname{edist}(x,y) < \\infty \\Rightarrow \\mathrm{efixedPoint}'(f,hsc,hsf,hfs x,hxs,hx) = \\mathrm{efixedPoint}'(f,htc,htf,hft y,hyt,hy).$$$
Lean4
/-- Let `f` be a contracting map with constant `K`; let `g` be another map uniformly
`C`-close to `f`. If `x` and `y` are their fixed points, then `dist x y ≤ C / (1 - K)`. -/
theorem dist_fixedPoint_fixedPoint_of_dist_le' (g : α → α) {x y} (hx : IsFixedPt f x) (hy : IsFixedPt g y) {C}
(hfg : ∀ z, dist (f z) (g z) ≤ C) : dist x y ≤ C / (1 - K) :=
calc
dist x y = dist y x := dist_comm x y
_ ≤ dist y (f y) / (1 - K) := (hf.dist_le_of_fixedPoint y hx)
_ = dist (f y) (g y) / (1 - K) := by rw [hy.eq, dist_comm]
_ ≤ C / (1 - K) := (div_le_div_iff_of_pos_right hf.one_sub_K_pos).2 (hfg y)
