nndist_triangle — Mathlib

English

Triangle inequality for nonnegative distance: nndist x z ≤ nndist x y + nndist y z.

Русский

Неравенство треугольника для неотрицательного расстояния: nndist x z ≤ nndist x y + nndist y z.

LaTeX

$$$ nndist(x,z) \le nndist(x,y) + nndist(y,z) $$$

Lean4

/-- Triangle inequality for the nonnegative distance -/
theorem nndist_triangle (x y z : α) : nndist x z ≤ nndist x y + nndist y z :=
  dist_triangle _ _ _

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