English
If s and t are adjacent in G, the edge set of G.replaceVertex s t equals the original edge set modified by removing the incidence with t and adding edges from s to each neighbor of s, excluding the self-edge at (t,t).
Русский
Если s и t смежны в G, множество ребер графа после замены вершины s на t равно исходному множеству ребер, модифицированному путём удаления инцидентности к t и добавления ребер от s к каждому соседу s, за исключением самособранного ребра (t,t).
LaTeX
$$$ (G.replaceVertex s t).edgeSet = \Big( G.edgeSet \ incidenceSet(t) \Big) \cup \{ \operatorname{Sym2.mk}\{ fst := x, snd := t \} : x \in neighborSet(s) \} \setminus \{ \operatorname{Sym2.mk}\{ fst := t, snd := t \} \} $$$
Lean4
theorem edgeSet_replaceVertex_of_adj (ha : G.Adj s t) :
(G.replaceVertex s t).edgeSet = (G.edgeSet \ G.incidenceSet t ∪ (s(·, t)) '' (G.neighborSet s)) \ {s(t, t)} :=
by
ext e; refine e.inductionOn ?_
simp only [replaceVertex, mem_edgeSet, Set.mem_union, Set.mem_diff, mk'_mem_incidenceSet_iff]
intros; split_ifs; exacts [by simp_all, by aesop, by rw [adj_comm]; aesop, by aesop]
