English
In a finite graph, along an isPath p, if w' is in the support and adjacent appropriately, the second vertex of p equals w'.
Русский
В конечном графе вдоль пути isPath, если есть соответствующая поддержка и смежность, второй вершиной пути является w'.
LaTeX
$$p.IsPath ∧ (List.mem p.support w') ∧ (G.Adj v w') → p.snd = w'$$
Lean4
theorem snd_of_mem_support_of_isPath_of_adj [Finite V] {v w w' : V} (hcyc : G.IsCycles) (p : G.Walk v w) (hw : w ≠ w')
(hw' : w' ∈ p.support) (hp : p.IsPath) (hadj : G.Adj v w') : p.snd = w' := by
classical
apply hp.snd_of_toSubgraph_adj
rw [Walk.mem_support_iff_exists_getVert] at hw'
obtain ⟨n, ⟨rfl, hnl⟩⟩ := hw'
by_cases hn : n = 0 ∨ n = p.length
· aesop
have e : G.neighborSet (p.getVert n) ≃ p.toSubgraph.neighborSet (p.getVert n) :=
by
refine @Classical.ofNonempty _ ?_
rw [← Cardinal.eq, ← Set.cast_ncard (Set.toFinite _), ← Set.cast_ncard (Set.toFinite _),
hp.ncard_neighborSet_toSubgraph_internal_eq_two (by cutsat) (by cutsat), hcyc (Set.nonempty_of_mem hadj.symm)]
rw [Subgraph.adj_comm, Subgraph.adj_iff_of_neighborSet_equiv e (Set.toFinite _)]
exact hadj.symm
