dist_inequality — Mathlib

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 _ _) _

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