isPath — Mathlib

English

Let p be a path from v to u in G, and let e be the edge between u and v. If e is not already used in p, then the walk obtained by appending e to p, i.e., Walk.cons h p, is a cycle.

Русский

Пусть p — путь из v в u в графе G, и возьмём ребро e между u и v. Если это ребро не встречается в p, тогда добавление e в конец пути даёт цикл.

LaTeX

$$$ \forall {V} {G : SimpleGraph V} {u v : V} (p : G.Path v u) (h : G.Adj u v) (he : s(u,v) \notin (p : G.Walk v u).edges), (Walk.cons h p).IsCycle$$$

Lean4

@[simp]
protected theorem isPath {u v : V} (p : G.Path u v) : (p : G.Walk u v).IsPath :=
  p.property

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