dist_triangle — Mathlib

English

For any u, v, w, dist_G(u,w) ≤ dist_G(u,v) + dist_G(v,w).

Русский

Для любых вершин u, v, w выполняется неравенство треугольника: dist_G(u,w) ≤ dist_G(u,v) + dist_G(v,w).

LaTeX

$$$$ \mathrm{dist}_G(u,w) \le \mathrm{dist}_G(u,v) + \mathrm{dist}_G(v,w) $$$$

Lean4

protected theorem dist_triangle (hconn : G.Connected) : G.dist u w ≤ G.dist u v + G.dist v w :=
  by
  obtain ⟨p, hp⟩ := hconn.exists_walk_length_eq_dist u v
  obtain ⟨q, hq⟩ := hconn.exists_walk_length_eq_dist v w
  rw [← hp, ← hq, ← Walk.length_append]
  apply dist_le

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