Documentation

Mathlib.Combinatorics.SimpleGraph.Operations

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 #

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 G.edgeSet] [Fintype G'.edgeSet] :
G.edgeFinset.card = G'.edgeFinset.card
def SimpleGraph.replaceVertex {V : Type u_1} (G : SimpleGraph V) (s : V) (t : V) [DecidableEq 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 : SimpleGraph V) (s : V) (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 : 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 : V} {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 : V} {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)}
    instance SimpleGraph.instDecidableRelAdjReplaceVertex {V : Type u_1} (G : SimpleGraph V) {s : V} {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 : V} {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 : V} {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 : V} {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 : V} {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 : V} {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 : 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) :
      (SimpleGraph.edge s t).Adj v w (v = s w = t v = t w = s) v w
      instance SimpleGraph.instDecidableRelAdjEdge {V : Type u_1} (s : V) (t : V) [DecidableEq V] :
      Equations
      @[simp]
      theorem SimpleGraph.sup_edge_self {V : Type u_1} (G : SimpleGraph V) (s : V) :
      theorem SimpleGraph.edge_edgeSet_of_ne {V : Type u_1} {s : V} {t : V} (h : s t) :
      (SimpleGraph.edge s t).edgeSet = {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) :
      instance SimpleGraph.instFintypeElemSym2EdgeSetEdge {V : Type u_1} {s : V} {t : V} [DecidableEq V] :
      Fintype (SimpleGraph.edge s t).edgeSet
      Equations
      • SimpleGraph.instFintypeElemSym2EdgeSetEdge = .mpr inferInstance
      theorem SimpleGraph.edgeFinset_sup_edge {V : Type u_1} (G : SimpleGraph V) {s : V} {t : V} [Fintype V] [DecidableRel G.Adj] [Fintype (G SimpleGraph.edge s t).edgeSet] (hn : ¬G.Adj s t) (h : s t) :
      (G SimpleGraph.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 : V} {t : V} [Fintype V] [DecidableRel G.Adj] [Fintype (G SimpleGraph.edge s t).edgeSet] (hn : ¬G.Adj s t) (h : s t) :
      (G SimpleGraph.edge s t).edgeFinset.card = G.edgeFinset.card + 1