eq_or_edist_eq_top_of_fixedPoints

English

If x and y are fixed points of f for a contraction on a complete space, then either x = y or edist x y = ∞.

Русский

Если x и y — фиксированные точки сжимающего отображения на полном пространстве, то либо x = y, либо edist x y = ∞.

LaTeX

$$$ x = y \;\lor\; \mathrm{edist}(x,y) = \infty $$$

Lean4

theorem eq_or_edist_eq_top_of_fixedPoints (hf : ContractingWith K f) {x y} (hx : IsFixedPt f x) (hy : IsFixedPt f y) :
    x = y ∨ edist x y = ∞ := by
  refine or_iff_not_imp_right.2 fun h ↦ edist_le_zero.1 ?_
  simpa only [hx.eq, edist_self, add_zero, ENNReal.zero_div] using hf.edist_le_of_fixedPoint h hy

Похожие утверждения