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.

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

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

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

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

@[implicit_reducible]

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

Equations

• G.instDecidableRelAdjReplaceVertex = id inferInstance

theorem SimpleGraph.edgeFinset_replaceVertex_of_not_adj {V : Type u_1} (G : SimpleGraph V) {s t : V} [DecidableEq V] [Fintype 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 : SimpleGraph V) {s t : V} [DecidableEq V] [Fintype 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 : SimpleGraph V) {s t : V} [DecidableEq V] [Fintype 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 : SimpleGraph V) {s t : V} [DecidableEq V] [Fintype 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 : SimpleGraph V) {s t : V} [DecidableEq V] [Fintype 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 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 t v w : V) : (edge s t).Adj v w ↔ (v = s ∧ w = t ∨ v = t ∧ w = s) ∧ v ≠ w

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

theorem SimpleGraph.edge_comm {V : Type u_1} (s t : V) : edge s t = edge t s

@[implicit_reducible]

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

Equations

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

@[simp]

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

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

theorem SimpleGraph.lt_sup_edge {V : Type u_1} (G : SimpleGraph V) (s t : V) (hne : s ≠ t) (hn : ¬G.Adj s t) : G < G ⊔ edge s t

theorem SimpleGraph.edge_le_iff {V : Type u_1} (G : SimpleGraph V) {v w : V} : edge v w ≤ G ↔ v = w ∨ G.Adj v w

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

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

theorem SimpleGraph.disjoint_edge {V : Type u_1} (G : SimpleGraph V) {u v : V} : Disjoint G (edge u v) ↔ ¬G.Adj u v

theorem SimpleGraph.sdiff_edge {V : Type u_1} (G : SimpleGraph V) {u v : V} (h : ¬G.Adj u v) : G \ edge u v = G

theorem SimpleGraph.Subgraph.spanningCoe_sup_edge_le {V : Type u_1} (G : SimpleGraph V) {s t : V} {H : (G ⊔ edge s t).Subgraph} (h : ¬H.Adj s t) : H.spanningCoe ≤ G

@[implicit_reducible]

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

Equations

• SimpleGraph.instFintypeElemSym2EdgeSetEdge = ⋯.mpr inferInstance

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

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