dist_dist_dist_le_left — Mathlib

English

For any x,y,z in a metric space, dist(dist(x,z), dist(y,z)) ≤ dist(x,y).

Русский

Для любых x,y,z в метрическом пространстве выполняется неравенство dist(dist(x,z), dist(y,z)) ≤ dist(x,y).

LaTeX

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

Lean4

theorem dist_dist_dist_le_left (x y z : α) : dist (dist x z) (dist y z) ≤ dist x y :=
  abs_dist_sub_le ..

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