English
If s and t are not adjacent, the edgeFinset after replacing s by t equals edgeFinset(G) minus incidenceFinset(t) union image of neighborFinset(s) under the map x ↦ Sym2.mk(x,t).
Русский
Если s и t не смежны, множество ребер в финсет после замены s на t равно edgeFinset(G) минус incidenceFinset(t) объединённое с образами neighborFinset(s) по отображению x ↦ Sym2.mk(x,t).
LaTeX
$$$ (G.replaceVertex s t).edgeFinset = G.edgeFinset \ G.incidenceFinset t \cup \operatorname{image}(x \mapsto \operatorname{Sym2.mk}\{ fst := x, snd := t \})(G.neighborFinset s) $$$
Lean4
theorem edgeFinset_replaceVertex_of_not_adj (hn : ¬G.Adj s t) :
(G.replaceVertex s t).edgeFinset = G.edgeFinset \ G.incidenceFinset t ∪ (G.neighborFinset s).image (s(·, t)) :=
by
simp only [incidenceFinset, neighborFinset, ← Set.toFinset_diff, ← Set.toFinset_image, ← Set.toFinset_union]
exact Set.toFinset_congr (G.edgeSet_replaceVertex_of_not_adj hn)
