English
If a nonempty walk exists, then the start vertex is adjacent to the second vertex in the subgraph.
Русский
Если обход не пуст, начальная вершина смежна со второй вершиной подграфа.
LaTeX
$${u v} (w : G.Walk u v) (h : ¬w.Nil) : w.toSubgraph.Adj u w.snd$$
Lean4
theorem neighborSet_toSubgraph_internal {u} {i : ℕ} {p : G.Walk u u} (hpc : p.IsCycle) (h : i ≠ 0) (h' : i < p.length) :
p.toSubgraph.neighborSet (p.getVert i) = {p.getVert (i - 1), p.getVert (i + 1)} :=
by
have hadj1 := ((show i - 1 + 1 = i from by cutsat) ▸ p.toSubgraph_adj_getVert (by cutsat : (i - 1) < p.length)).symm
ext v
simp_all only [ne_eq, Subgraph.mem_neighborSet, Set.mem_insert_iff, Set.mem_singleton_iff,
SimpleGraph.Walk.toSubgraph_adj_iff, Sym2.eq, Sym2.rel_iff', Prod.mk.injEq, Prod.swap_prod_mk]
refine ⟨?_, by aesop⟩
rintro ⟨i', ⟨hl1, hl2⟩ | ⟨hr1, hr2⟩⟩
· apply hpc.getVert_injOn' (by rw [Set.mem_setOf_eq]; cutsat) (by rw [Set.mem_setOf_eq]; cutsat)at hl1
simp_all
· apply hpc.getVert_injOn (by rw [Set.mem_setOf_eq]; cutsat) (by rw [Set.mem_setOf_eq]; cutsat)at hr2
aesop
