exists_isCycle_snd_verts_eq — Mathlib

English

Given a cycle p and an adjacency p.toSubgraph.Adj v w, there exists a walk p' with matching vertex set and appropriate endpoints.

Русский

При наличии смежности между вершинами, существует обход с тем же множеством вершин и корректными концами.

LaTeX

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

Lean4

theorem exists_isCycle_snd_verts_eq {p : G.Walk v v} (h : p.IsCycle) (hadj : p.toSubgraph.Adj v w) :
    ∃ (p' : G.Walk v v), p'.IsCycle ∧ p'.snd = w ∧ p'.toSubgraph.verts = p.toSubgraph.verts :=
  by
  have : w ∈ p.toSubgraph.neighborSet v := hadj
  rw [h.neighborSet_toSubgraph_endpoint] at this
  simp only [Set.mem_insert_iff, Set.mem_singleton_iff] at this
  obtain hl | hr := this
  · exact ⟨p, ⟨h, hl.symm, rfl⟩⟩
  · use p.reverse
    rw [penultimate, ← getVert_reverse] at hr
    exact ⟨h.reverse, hr.symm, by rw [toSubgraph_reverse _]⟩

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