English
If edist x (f x), edist y (f y) are finite and edist x y is finite, then fixed points agree: efixedPoint x = efixedPoint y.
Русский
Если edist x (f x), edist y (f y) конечны и edist x y конечен, то efixedPoint x = efixedPoint y.
LaTeX
$$$ edist x y < \infty \land edist x (f x) < \infty \land edist y (f y) < \infty \Rightarrow efixedPoint f hf x hx = efixedPoint f hf y hy $$$
Lean4
theorem efixedPoint_eq_of_edist_lt_top (hf : ContractingWith K f) {x : α} (hx : edist x (f x) ≠ ∞) {y : α}
(hy : edist y (f y) ≠ ∞) (h : edist x y ≠ ∞) : efixedPoint f hf x hx = efixedPoint f hf y 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'
exact hf.edist_efixedPoint_lt_top hx
trans y
exacts [lt_top_iff_ne_top.2 h, hf.edist_efixedPoint_lt_top hy]
