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 : SimpleGraph V} {W : Type u_2} {G' : SimpleGraph W} (f : G ≃g G') [Fintype ↑(SimpleGraph.edgeSet G)] [Fintype ↑(SimpleGraph.edgeSet G')] : (SimpleGraph.edgeFinset G).card = (SimpleGraph.edgeFinset G').card

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 = { 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 := ⋯ }

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.edge {V : Type u_1} (s : V) (t : V) : SimpleGraph V

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

Equations

• SimpleGraph.edge s t = SimpleGraph.fromEdgeSet {s(s, t)}

theorem SimpleGraph.edge_adj {V : Type u_1} (s : V) (t : V) (v : V) (w : V) : (SimpleGraph.edge s t).Adj v w ↔ (v = s ∧ w = t ∨ v = t ∧ w = s) ∧ v ≠ w

instance SimpleGraph.instDecidableRelAdjEdge {V : Type u_1} [DecidableEq V] (s : V) (t : V) : DecidableRel (SimpleGraph.edge s t).Adj

Equations

• SimpleGraph.instDecidableRelAdjEdge s t x✝ x = Eq.mpr ⋯ inferInstance

theorem SimpleGraph.edge_self_eq_bot {V : Type u_1} (s : V) : SimpleGraph.edge s s = ⊥

@[simp]

theorem SimpleGraph.sup_edge_self {V : Type u_1} (G : SimpleGraph V) (s : V) : G ⊔ SimpleGraph.edge s s = G

theorem SimpleGraph.edge_edgeSet_of_ne {V : Type u_1} {s : V} {t : V} (h : s ≠ t) : SimpleGraph.edgeSet (SimpleGraph.edge s t) = {s(s, t)}

theorem SimpleGraph.sup_edge_of_adj {V : Type u_1} (G : SimpleGraph V) {s : V} {t : V} (h : G.Adj s t) : G ⊔ SimpleGraph.edge s t = G

instance SimpleGraph.instFintypeElemSym2EdgeSetEdge {V : Type u_1} [DecidableEq V] {s : V} {t : V} : Fintype ↑(SimpleGraph.edgeSet (SimpleGraph.edge s t))

Equations

• SimpleGraph.instFintypeElemSym2EdgeSetEdge = Eq.mpr ⋯ inferInstance

theorem SimpleGraph.edgeFinset_sup_edge {V : Type u_1} (G : SimpleGraph V) {s : V} {t : V} [Fintype V] [DecidableRel G.Adj] [Fintype ↑(SimpleGraph.edgeSet (G ⊔ SimpleGraph.edge s t))] (hn : ¬G.Adj s t) (h : s ≠ t) : SimpleGraph.edgeFinset (G ⊔ SimpleGraph.edge s t) = Finset.cons s(s, t) (SimpleGraph.edgeFinset G) ⋯

theorem SimpleGraph.card_edgeFinset_sup_edge {V : Type u_1} (G : SimpleGraph V) {s : V} {t : V} [Fintype V] [DecidableRel G.Adj] [Fintype ↑(SimpleGraph.edgeSet (G ⊔ SimpleGraph.edge s t))] (hn : ¬G.Adj s t) (h : s ≠ t) : (SimpleGraph.edgeFinset (G ⊔ SimpleGraph.edge s t)).card = (SimpleGraph.edgeFinset G).card + 1