exists_isPath — Mathlib

English

For a preconnected graph, between any two vertices u and v there exists a walk p from u to v that is a path.

Русский

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

LaTeX

$$$\forall G\; (h : G.Preconnected)\; \forall u v, \exists p : G.Walk u v, p.IsPath$$$

Lean4

theorem exists_isPath {G : SimpleGraph V} (h : G.Preconnected) (u v : V) : ∃ p : G.Walk u v, p.IsPath :=
  (h u v).exists_isPath

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