neighborSet_toSubgraph_endpoint — Mathlib

English

If p is a cycle, there exists a walk with a specified second vertex and matching vertex set, ensuring a continuation of the cycle.

Русский

Если p — цикл, существует обход с заданной второй вершиной и совпадающим множеством вершин, сохраняющий цикл.

LaTeX

$$$\exists p' : G.Walk\ v\ v , p'.IsCycle ∧ p'.snd = w ∧ p'.toSubgraph.verts = p.toSubgraph.verts$$$

Lean4

theorem neighborSet_toSubgraph_endpoint {u v} {p : G.Walk u v} (hp : p.IsPath) (hnp : ¬p.Nil) :
    p.toSubgraph.neighborSet v = { p.penultimate } := by
  simpa using
    IsPath.neighborSet_toSubgraph_startpoint hp.reverse
      (by rw [Walk.not_nil_iff_lt_length, Walk.length_reverse]; exact Walk.not_nil_iff_lt_length.mp hnp)

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