English
For a contracting map f with constant K, the distance between any x,y is bounded by (d(x,f x) + d(y,f y)) / (1 − K).
Русский
Для сжимающего отображения f константы K предел расстояния d(x,y) ≤ (d(x,f x) + d(y,f y)) / (1 − K).
LaTeX
$$$d(x,y) \\le \\dfrac{d(x,f x) + d(y,f y)}{1 - K}.$$$
Lean4
theorem dist_inequality (x y) : dist x y ≤ (dist x (f x) + dist y (f y)) / (1 - K) :=
suffices dist x y ≤ dist x (f x) + dist y (f y) + K * dist x y by
rwa [le_div_iff₀ hf.one_sub_K_pos, mul_comm, _root_.sub_mul, one_mul, sub_le_iff_le_add]
calc
dist x y ≤ dist x (f x) + dist y (f y) + dist (f x) (f y) := dist_triangle4_right _ _ _ _
_ ≤ dist x (f x) + dist y (f y) + K * dist x y := add_le_add_left (hf.dist_le_mul _ _) _