dist_dist_dist_le — Mathlib

English

For any x,y,x',y' the distance between dist(x,y) and dist(x',y') is bounded by dist(x,x')+dist(y,y').

Русский

Для любых x,y,x',y' неравенство: dist(dist(x,y), dist(x',y')) ≤ dist(x,x') + dist(y,y').

LaTeX

$$$\operatorname{dist}(\operatorname{dist}(x,y), \operatorname{dist}(x',y')) \le \operatorname{dist}(x,x') + \operatorname{dist}(y,y')$$$

Lean4

theorem dist_dist_dist_le (x y x' y' : α) : dist (dist x y) (dist x' y') ≤ dist x x' + dist y y' :=
  (dist_triangle _ _ _).trans <| add_le_add (dist_dist_dist_le_left _ _ _) (dist_dist_dist_le_right _ _ _)

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