English
For a path p with i ≠ 0 and i < length(p), the neighbor set at vertex i equals the two neighboring vertices i-1 and i+1.
Русский
Для пути p при i ≠ 0 и i < length(p) множество соседей вершины i равно вершинам i-1 и i+1.
LaTeX
$$$ p.IsPath \Rightarrow i \neq 0 \Rightarrow i < p.length \Rightarrow p.toSubgraph.neighborSet (p.getVert i) = \{ p.getVert (i-1), p.getVert (i+1) \}$$$
Lean4
theorem neighborSet_toSubgraph_internal {u} {i : ℕ} {p : G.Walk u v} (hp : p.IsPath) (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', ⟨hl, _⟩ | ⟨_, hl⟩⟩ <;>
apply hp.getVert_injOn (by rw [Set.mem_setOf_eq]; cutsat) (by rw [Set.mem_setOf_eq]; cutsat)at hl <;>
aesop
