English
If w is a nonempty path, then the second vertex is determined by the adjacency relation from the first vertex within the subgraph.
Русский
Если путь непуст, вторая вершина определяется по смежности в подграфе от первой вершины.
LaTeX
$$$ w.toSubgraph.Adj u w.snd $$$
Lean4
theorem neighborSet_toSubgraph_endpoint {u} {p : G.Walk u u} (hpc : p.IsCycle) :
p.toSubgraph.neighborSet u = { p.snd, p.penultimate } :=
by
have hadj1 := p.toSubgraph_adj_snd hpc.not_nil
have hadj2 := (p.toSubgraph_adj_penultimate hpc.not_nil).symm
ext v
simp_all only [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 | hr⟩
· rw [hpc.getVert_endpoint_iff (by cutsat)] at hl
cases hl.1 <;> aesop
· rcases (hpc.getVert_endpoint_iff (by cutsat)).mp hr.2 with h1 | h2
· contradiction
· simp only [penultimate, ← h2, add_tsub_cancel_right]
simp_all
