edist_triangle4 — Mathlib

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

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