exists_walk_length_eq_edist — Mathlib

English

If G is connected, for any u,v, there exists a walk p from u to v with length equal to G.edist u v.

Русский

Если граф связный, для любых вершин u,v существует путь от u до v длиной, равной edist u v.

LaTeX

$$$ (\text{G is connected}) \Rightarrow \forall u,v, \exists p : G.Walk u v, p.length = G.edist u v $$$

Lean4

protected theorem exists_walk_length_eq_edist (hconn : G.Connected) (u v : V) :
    ∃ p : G.Walk u v, p.length = G.edist u v :=
  (hconn u v).exists_walk_length_eq_edist

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