# Local graph operations #

This file defines some single-graph operations that modify a finite number of vertices and proves basic theorems about them. When the graph itself has a finite number of vertices we also prove theorems about the number of edges in the modified graphs.

## Main definitions #

• G.replaceVertex s t is G with t replaced by a copy of s, removing the s-t edge if present.
• edge s t is the graph with a single s-t edge. Adding this edge to a graph G is then G ⊔ edge s t.
theorem SimpleGraph.Iso.card_edgeFinset_eq {V : Type u_1} {G : } {W : Type u_2} {G' : } (f : G ≃g G') [Fintype G.edgeSet] [Fintype G'.edgeSet] :
G.edgeFinset.card = G'.edgeFinset.card
def SimpleGraph.replaceVertex {V : Type u_1} [] (G : ) (s : V) (t : V) :

The graph formed by forgetting t's neighbours and instead giving it those of s. The s-t edge is removed if present.

Equations
• G.replaceVertex s t = { Adj := fun (v w : V) => if v = t then if w = t then False else G.Adj s w else if w = t then G.Adj v s else G.Adj v w, symm := , loopless := }
Instances For
theorem SimpleGraph.not_adj_replaceVertex_same {V : Type u_1} [] (G : ) (s : V) (t : V) :

There is never an s-t edge in G.replaceVertex s t.

@[simp]
theorem SimpleGraph.replaceVertex_self {V : Type u_1} [] (G : ) (s : V) :
G.replaceVertex s s = G
theorem SimpleGraph.adj_replaceVertex_iff_of_ne_left {V : Type u_1} [] (G : ) (s : V) {t : V} {w : V} (hw : w t) :

Except possibly for t, the neighbours of s in G.replaceVertex s t are its neighbours in G.

theorem SimpleGraph.adj_replaceVertex_iff_of_ne_right {V : Type u_1} [] (G : ) (s : V) {t : V} {w : V} (hw : w t) :

Except possibly for itself, the neighbours of t in G.replaceVertex s t are the neighbours of s in G.

theorem SimpleGraph.adj_replaceVertex_iff_of_ne {V : Type u_1} [] (G : ) (s : V) {t : V} {v : V} {w : V} (hv : v t) (hw : w t) :

Adjacency in G.replaceVertex s t which does not involve t is the same as that of G.

theorem SimpleGraph.edgeSet_replaceVertex_of_not_adj {V : Type u_1} [] (G : ) {s : V} {t : V} (hn : ¬G.Adj s t) :
(G.replaceVertex s t).edgeSet = G.edgeSet \ G.incidenceSet t (fun (x : V) => s(x, t)) '' G.neighborSet s
theorem SimpleGraph.edgeSet_replaceVertex_of_adj {V : Type u_1} [] (G : ) {s : V} {t : V} (ha : G.Adj s t) :
(G.replaceVertex s t).edgeSet = (G.edgeSet \ G.incidenceSet t (fun (x : V) => s(x, t)) '' G.neighborSet s) \ {s(t, t)}
instance SimpleGraph.instDecidableRelAdjReplaceVertex {V : Type u_1} [] (G : ) {s : V} {t : V} [DecidableRel G.Adj] :
Equations
theorem SimpleGraph.edgeFinset_replaceVertex_of_not_adj {V : Type u_1} [] (G : ) {s : V} {t : V} [] [DecidableRel G.Adj] (hn : ¬G.Adj s t) :
(G.replaceVertex s t).edgeFinset = G.edgeFinset \ G.incidenceFinset t Finset.image (fun (x : V) => s(x, t)) (G.neighborFinset s)
theorem SimpleGraph.edgeFinset_replaceVertex_of_adj {V : Type u_1} [] (G : ) {s : V} {t : V} [] [DecidableRel G.Adj] (ha : G.Adj s t) :
(G.replaceVertex s t).edgeFinset = (G.edgeFinset \ G.incidenceFinset t Finset.image (fun (x : V) => s(x, t)) (G.neighborFinset s)) \ {s(t, t)}
theorem SimpleGraph.disjoint_sdiff_neighborFinset_image {V : Type u_1} [] (G : ) {s : V} {t : V} [] [DecidableRel G.Adj] :
Disjoint (G.edgeFinset \ G.incidenceFinset t) (Finset.image (fun (x : V) => s(x, t)) (G.neighborFinset s))
theorem SimpleGraph.card_edgeFinset_replaceVertex_of_not_adj {V : Type u_1} [] (G : ) {s : V} {t : V} [] [DecidableRel G.Adj] (hn : ¬G.Adj s t) :
(G.replaceVertex s t).edgeFinset.card = G.edgeFinset.card + G.degree s - G.degree t
theorem SimpleGraph.card_edgeFinset_replaceVertex_of_adj {V : Type u_1} [] (G : ) {s : V} {t : V} [] [DecidableRel G.Adj] (ha : G.Adj s t) :
(G.replaceVertex s t).edgeFinset.card = G.edgeFinset.card + G.degree s - G.degree t - 1
def SimpleGraph.edge {V : Type u_1} (s : V) (t : V) :

The graph with a single s-t edge. It is empty iff s = t.

Equations
Instances For
theorem SimpleGraph.edge_adj {V : Type u_1} (s : V) (t : V) (v : V) (w : V) :
().Adj v w (v = s w = t v = t w = s) v w
instance SimpleGraph.instDecidableRelAdjEdge {V : Type u_1} [] (s : V) (t : V) :
Equations
• = .mpr inferInstance
theorem SimpleGraph.edge_self_eq_bot {V : Type u_1} (s : V) :
@[simp]
theorem SimpleGraph.sup_edge_self {V : Type u_1} (G : ) (s : V) :
G = G
theorem SimpleGraph.edge_edgeSet_of_ne {V : Type u_1} {s : V} {t : V} (h : s t) :
().edgeSet = {s(s, t)}
theorem SimpleGraph.sup_edge_of_adj {V : Type u_1} (G : ) {s : V} {t : V} (h : G.Adj s t) :
G = G
instance SimpleGraph.instFintypeElemSym2EdgeSetEdge {V : Type u_1} [] {s : V} {t : V} :
Fintype ().edgeSet
Equations
• SimpleGraph.instFintypeElemSym2EdgeSetEdge = .mpr inferInstance
theorem SimpleGraph.edgeFinset_sup_edge {V : Type u_1} (G : ) {s : V} {t : V} [] [DecidableRel G.Adj] [Fintype (G ).edgeSet] (hn : ¬G.Adj s t) (h : s t) :
(G ).edgeFinset = Finset.cons s(s, t) G.edgeFinset
theorem SimpleGraph.card_edgeFinset_sup_edge {V : Type u_1} (G : ) {s : V} {t : V} [] [DecidableRel G.Adj] [Fintype (G ).edgeSet] (hn : ¬G.Adj s t) (h : s t) :
(G ).edgeFinset.card = G.edgeFinset.card + 1