English
If a contracting map f on S has two forward-invariant contracting restrictions with fixed seeds x ∈ S and y ∈ T, and the distances to their images are finite as well as the distance between x and y, then the efixedPoint' constructed from x on S equals the efixedPoint' constructed from y on T.
Русский
Если сжимающее отображение f на S имеет двеForward-invariant ограниченных области с фиктивными стартами x и y и при этом расстояние между этими стартами конечное, то фиксированные точки совпадут.
LaTeX
$$$\\mathrm{efixedPoint}'(f,hsc,hsf,hfs\\ x,hxs,hx) = \\mathrm{efixedPoint}'(f,htc,htf,hft\\ y,hyt,hy).$$$
Lean4
/-- If a globally contracting map `f` has two complete forward-invariant sets `s`, `t`,
and `x ∈ s` is at a finite distance from `y ∈ t`, then the `efixedPoint'` constructed by `x`
is the same as the `efixedPoint'` constructed by `y`.
This lemma takes additional arguments stating that `f` contracts on `s` and `t` because this way
it can be used to prove the desired equality with non-trivial proofs of these facts. -/
theorem efixedPoint_eq_of_edist_lt_top' (hf : ContractingWith K f) {s : Set α} (hsc : IsComplete s) (hsf : MapsTo f s s)
(hfs : ContractingWith K <| hsf.restrict f s s) {x : α} (hxs : x ∈ s) (hx : edist x (f x) ≠ ∞) {t : Set α}
(htc : IsComplete t) (htf : MapsTo f t t) (hft : ContractingWith K <| htf.restrict f t t) {y : α} (hyt : y ∈ t)
(hy : edist y (f y) ≠ ∞) (hxy : edist x y ≠ ∞) :
efixedPoint' f hsc hsf hfs x hxs hx = efixedPoint' f htc htf hft y hyt hy :=
by
refine (hf.eq_or_edist_eq_top_of_fixedPoints ?_ ?_).elim id fun h' ↦ False.elim (ne_of_lt ?_ h') <;>
try apply efixedPoint_isFixedPt'
change edistLtTopSetoid _ _
trans x
· apply Setoid.symm'
apply edist_efixedPoint_lt_top'
trans y
· exact lt_top_iff_ne_top.2 hxy
· apply edist_efixedPoint_lt_top'
