English
Extended triangle inequality chaining: edist x t ≤ edist x y + edist y z + edist z t.
Русский
Неравенство треугольника в ланцюге: edist x t ≤ edist x y + edist y z + edist z t.
LaTeX
$$$ edist\ x\ t \leq edist\ x\ y + edist\ y\ z + edist\ z\ t $$$
Lean4
theorem edist_triangle4 (x y z t : α) : edist x t ≤ edist x y + edist y z + edist z t :=
calc
edist x t ≤ edist x z + edist z t := edist_triangle x z t
_ ≤ edist x y + edist y z + edist z t := add_le_add_right (edist_triangle x y z) _