edist_le_of_fixedPoint — Mathlib

English

If y is a fixed point of f and edist x y is finite, then edist x y is bounded by edist x f x divided by (1 − K).

Русский

Если y — фиксированная точка f и edist x y конечна, то edist x y ≤ edist x f x /(1 − K).

LaTeX

$$$ \mathrm{edist}(x,y) \le \mathrm{edist}(x,f(x)) / (1 - K)$$$

Lean4

theorem edist_le_of_fixedPoint (hf : ContractingWith K f) {x y} (h : edist x y ≠ ∞) (hy : IsFixedPt f y) :
    edist x y ≤ edist x (f x) / (1 - K) := by simpa only [hy.eq, edist_self, add_zero] using hf.edist_inequality h

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