dist_le_of_fixedPoint — Mathlib

English

If f is contracting, then the distance from x to the fixed point of f is bounded by dist(x,f x) /(1 − K).

Русский

Если f сжатие, то расстояние от x до фиксированной точки удовлетворяет неравенству dist(x, f x)/(1 − K).

LaTeX

$$$\\operatorname{dist}\\bigl(x, \\mathrm{fixedPoint}(f,hf)\\bigr) \\le \\dfrac{\\operatorname{dist}(x,f x)}{1 - K}.$$$

Lean4

theorem dist_le_of_fixedPoint (x) {y} (hy : IsFixedPt f y) : dist x y ≤ dist x (f x) / (1 - K) := by
  simpa only [hy.eq, dist_self, add_zero] using hf.dist_inequality x y

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