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.
• G.addEdge s t is G with the s-t edge added, if that is a valid edge.

def SimpleGraph.replaceVertex {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) (s : V) (t : V) : SimpleGraph 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

• SimpleGraph.replaceVertex G s t = SimpleGraph.mk 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

theorem SimpleGraph.not_adj_replaceVertex_same {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) (s : V) (t : V) : ¬(SimpleGraph.replaceVertex G s t).Adj s t

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

@[simp]

theorem SimpleGraph.replaceVertex_self {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) (s : V) : SimpleGraph.replaceVertex G s s = G

theorem SimpleGraph.adj_replaceVertex_iff_of_ne_left {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) (s : V) {t : V} {w : V} (hw : w ≠ t) : (SimpleGraph.replaceVertex G s t).Adj s w ↔ G.Adj s w

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} [DecidableEq V] (G : SimpleGraph V) (s : V) {t : V} {w : V} (hw : w ≠ t) : (SimpleGraph.replaceVertex G s t).Adj t w ↔ G.Adj s w

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} [DecidableEq V] (G : SimpleGraph V) (s : V) {t : V} {v : V} {w : V} (hv : v ≠ t) (hw : w ≠ t) : (SimpleGraph.replaceVertex G s t).Adj v w ↔ G.Adj v w

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} [DecidableEq V] (G : SimpleGraph V) {s : V} {t : V} (hn : ¬G.Adj s t) : SimpleGraph.edgeSet (SimpleGraph.replaceVertex G s t) = SimpleGraph.edgeSet G \ SimpleGraph.incidenceSet G t ∪ (fun (x : V) => s(x, t)) '' SimpleGraph.neighborSet G s

theorem SimpleGraph.edgeSet_replaceVertex_of_adj {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) {s : V} {t : V} (ha : G.Adj s t) : SimpleGraph.edgeSet (SimpleGraph.replaceVertex G s t) = (SimpleGraph.edgeSet G \ SimpleGraph.incidenceSet G t ∪ (fun (x : V) => s(x, t)) '' SimpleGraph.neighborSet G s) \ {s(t, t)}

instance SimpleGraph.instDecidableRelAdjReplaceVertex {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) {s : V} {t : V} [DecidableRel G.Adj] : DecidableRel (SimpleGraph.replaceVertex G s t).Adj

Equations

• SimpleGraph.instDecidableRelAdjReplaceVertex G = id inferInstance

theorem SimpleGraph.edgeFinset_replaceVertex_of_not_adj {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) {s : V} {t : V} [Fintype V] [DecidableRel G.Adj] (hn : ¬G.Adj s t) : SimpleGraph.edgeFinset (SimpleGraph.replaceVertex G s t) = SimpleGraph.edgeFinset G \ SimpleGraph.incidenceFinset G t ∪ Finset.image (fun (x : V) => s(x, t)) (SimpleGraph.neighborFinset G s)

theorem SimpleGraph.edgeFinset_replaceVertex_of_adj {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) {s : V} {t : V} [Fintype V] [DecidableRel G.Adj] (ha : G.Adj s t) : SimpleGraph.edgeFinset (SimpleGraph.replaceVertex G s t) = (SimpleGraph.edgeFinset G \ SimpleGraph.incidenceFinset G t ∪ Finset.image (fun (x : V) => s(x, t)) (SimpleGraph.neighborFinset G s)) \ {s(t, t)}

theorem SimpleGraph.disjoint_sdiff_neighborFinset_image {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) {s : V} {t : V} [Fintype V] [DecidableRel G.Adj] : Disjoint (SimpleGraph.edgeFinset G \ SimpleGraph.incidenceFinset G t) (Finset.image (fun (x : V) => s(x, t)) (SimpleGraph.neighborFinset G s))

theorem SimpleGraph.card_edgeFinset_replaceVertex_of_not_adj {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) {s : V} {t : V} [Fintype V] [DecidableRel G.Adj] (hn : ¬G.Adj s t) : (SimpleGraph.edgeFinset (SimpleGraph.replaceVertex G s t)).card = (SimpleGraph.edgeFinset G).card + SimpleGraph.degree G s - SimpleGraph.degree G t

theorem SimpleGraph.card_edgeFinset_replaceVertex_of_adj {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) {s : V} {t : V} [Fintype V] [DecidableRel G.Adj] (ha : G.Adj s t) : (SimpleGraph.edgeFinset (SimpleGraph.replaceVertex G s t)).card = (SimpleGraph.edgeFinset G).card + SimpleGraph.degree G s - SimpleGraph.degree G t - 1

def SimpleGraph.addEdge {V : Type u_1} (G : SimpleGraph V) (s : V) (t : V) : SimpleGraph V

Given a vertex pair, add the corresponding edge to the graph's edge set if not present.

Equations

• SimpleGraph.addEdge G s t = SimpleGraph.mk fun (v w : V) => G.Adj v w ∨ s ≠ t ∧ (s = v ∧ t = w ∨ s = w ∧ t = v)

@[simp]

theorem SimpleGraph.addEdge_self {V : Type u_1} (G : SimpleGraph V) (s : V) : SimpleGraph.addEdge G s s = G

theorem SimpleGraph.addEdge_of_adj {V : Type u_1} (G : SimpleGraph V) {s : V} {t : V} (h : G.Adj s t) : SimpleGraph.addEdge G s t = G

instance SimpleGraph.instDecidableRelAdjAddEdge {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) {s : V} {t : V} [DecidableRel G.Adj] : DecidableRel (SimpleGraph.addEdge G s t).Adj

Equations

• SimpleGraph.instDecidableRelAdjAddEdge G = id inferInstance

theorem SimpleGraph.edgeFinset_addEdge {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) {s : V} {t : V} [Fintype V] [DecidableRel G.Adj] (hn : ¬G.Adj s t) (h : s ≠ t) : SimpleGraph.edgeFinset (SimpleGraph.addEdge G s t) = Finset.cons s(s, t) (SimpleGraph.edgeFinset G) (_ : s(s, t) ∉ Set.toFinset (SimpleGraph.edgeSet G))

theorem SimpleGraph.card_edgeFinset_addEdge {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) {s : V} {t : V} [Fintype V] [DecidableRel G.Adj] (hn : ¬G.Adj s t) (h : s ≠ t) : (SimpleGraph.edgeFinset (SimpleGraph.addEdge G s t)).card = (SimpleGraph.edgeFinset G).card + 1