# Subgraphs of a simple graph #

A subgraph of a simple graph consists of subsets of the graph's vertices and edges such that the endpoints of each edge are present in the vertex subset. The edge subset is formalized as a sub-relation of the adjacency relation of the simple graph.

## Implementation notes #

• Recall that subgraphs are not determined by their vertex sets, so SetLike does not apply to this kind of subobject.

## Todo #

• Images of graph homomorphisms as subgraphs.
theorem SimpleGraph.Subgraph.ext {V : Type u} {G : } (x : G.Subgraph) (y : G.Subgraph) (verts : x.verts = y.verts) (Adj : x.Adj = y.Adj) :
x = y
theorem SimpleGraph.Subgraph.ext_iff {V : Type u} {G : } (x : G.Subgraph) (y : G.Subgraph) :
structure SimpleGraph.Subgraph {V : Type u} (G : ) :

A subgraph of a SimpleGraph is a subset of vertices along with a restriction of the adjacency relation that is symmetric and is supported by the vertex subset. They also form a bounded lattice.

Thinking of V → V → Prop as Set (V × V), a set of darts (i.e., half-edges), then Subgraph.adj_sub is that the darts of a subgraph are a subset of the darts of G.

• verts : Set V
• edge_vert : ∀ {v w : V}, self.Adj v wv self.verts
Instances For
theorem SimpleGraph.Subgraph.adj_sub {V : Type u} {G : } (self : G.Subgraph) {v : V} {w : V} :
theorem SimpleGraph.Subgraph.edge_vert {V : Type u} {G : } (self : G.Subgraph) {v : V} {w : V} :
theorem SimpleGraph.Subgraph.symm {V : Type u} {G : } (self : G.Subgraph) :
@[simp]
theorem SimpleGraph.singletonSubgraph_adj {V : Type u} (G : ) (v : V) :
∀ (a a_1 : V), (G.singletonSubgraph v).Adj a a_1 = a a_1
@[simp]
theorem SimpleGraph.singletonSubgraph_verts {V : Type u} (G : ) (v : V) :
(G.singletonSubgraph v).verts = {v}
def SimpleGraph.singletonSubgraph {V : Type u} (G : ) (v : V) :
G.Subgraph

The one-vertex subgraph.

Equations
• G.singletonSubgraph v = { verts := {v}, Adj := , adj_sub := , edge_vert := , symm := }
Instances For
@[simp]
theorem SimpleGraph.subgraphOfAdj_verts {V : Type u} (G : ) {v : V} {w : V} (hvw : G.Adj v w) :
@[simp]
theorem SimpleGraph.subgraphOfAdj_adj {V : Type u} (G : ) {v : V} {w : V} (hvw : G.Adj v w) (a : V) (b : V) :
def SimpleGraph.subgraphOfAdj {V : Type u} (G : ) {v : V} {w : V} (hvw : G.Adj v w) :
G.Subgraph

The one-edge subgraph.

Equations
• G.subgraphOfAdj hvw = { verts := {v, w}, Adj := fun (a b : V) => s(v, w) = s(a, b), adj_sub := , edge_vert := , symm := }
Instances For
theorem SimpleGraph.Subgraph.loopless {V : Type u} {G : } (G' : G.Subgraph) :
theorem SimpleGraph.Subgraph.adj_comm {V : Type u} {G : } (G' : G.Subgraph) (v : V) (w : V) :
theorem SimpleGraph.Subgraph.adj_symm {V : Type u} {G : } (G' : G.Subgraph) {u : V} {v : V} (h : G'.Adj u v) :
theorem SimpleGraph.Subgraph.Adj.symm {V : Type u} {G : } {G' : G.Subgraph} {u : V} {v : V} (h : G'.Adj u v) :
theorem SimpleGraph.Subgraph.Adj.adj_sub {V : Type u} {G : } {H : G.Subgraph} {u : V} {v : V} (h : H.Adj u v) :
theorem SimpleGraph.Subgraph.Adj.fst_mem {V : Type u} {G : } {H : G.Subgraph} {u : V} {v : V} (h : H.Adj u v) :
u H.verts
theorem SimpleGraph.Subgraph.Adj.snd_mem {V : Type u} {G : } {H : G.Subgraph} {u : V} {v : V} (h : H.Adj u v) :
v H.verts
theorem SimpleGraph.Subgraph.Adj.ne {V : Type u} {G : } {H : G.Subgraph} {u : V} {v : V} (h : H.Adj u v) :
u v
@[simp]
theorem SimpleGraph.Subgraph.coe_adj {V : Type u} {G : } (G' : G.Subgraph) (v : G'.verts) (w : G'.verts) :
def SimpleGraph.Subgraph.coe {V : Type u} {G : } (G' : G.Subgraph) :
SimpleGraph G'.verts

Coercion from G' : Subgraph G to a SimpleGraph G'.verts.

Equations
• G'.coe = { Adj := fun (v w : G'.verts) => G'.Adj v w, symm := , loopless := }
Instances For
@[simp]
theorem SimpleGraph.Subgraph.coe_adj_sub {V : Type u} {G : } (G' : G.Subgraph) (u : G'.verts) (v : G'.verts) (h : G'.coe.Adj u v) :
theorem SimpleGraph.Subgraph.Adj.coe {V : Type u} {G : } {H : G.Subgraph} {u : V} {v : V} (h : H.Adj u v) :
def SimpleGraph.Subgraph.IsSpanning {V : Type u} {G : } (G' : G.Subgraph) :

A subgraph is called a spanning subgraph if it contains all the vertices of G.

Equations
• G'.IsSpanning = ∀ (v : V), v G'.verts
Instances For
theorem SimpleGraph.Subgraph.isSpanning_iff {V : Type u} {G : } {G' : G.Subgraph} :
G'.IsSpanning G'.verts = Set.univ
@[simp]
theorem SimpleGraph.Subgraph.spanningCoe_adj {V : Type u} {G : } (G' : G.Subgraph) :
∀ (a a_1 : V), G'.spanningCoe.Adj a a_1 = G'.Adj a a_1
def SimpleGraph.Subgraph.spanningCoe {V : Type u} {G : } (G' : G.Subgraph) :

Coercion from Subgraph G to SimpleGraph V. If G' is a spanning subgraph, then G'.spanningCoe yields an isomorphic graph. In general, this adds in all vertices from V as isolated vertices.

Equations
• G'.spanningCoe = { Adj := G'.Adj, symm := , loopless := }
Instances For
@[simp]
theorem SimpleGraph.Subgraph.Adj.of_spanningCoe {V : Type u} {G : } {G' : G.Subgraph} {u : G'.verts} {v : G'.verts} (h : G'.spanningCoe.Adj u v) :
theorem SimpleGraph.Subgraph.spanningCoe_inj {V : Type u} {G : } {G₁ : G.Subgraph} {G₂ : G.Subgraph} :
@[simp]
theorem SimpleGraph.Subgraph.spanningCoeEquivCoeOfSpanning_apply_coe {V : Type u} {G : } (G' : G.Subgraph) (h : G'.IsSpanning) (v : V) :
((G'.spanningCoeEquivCoeOfSpanning h) v) = v
@[simp]
theorem SimpleGraph.Subgraph.spanningCoeEquivCoeOfSpanning_symm_apply {V : Type u} {G : } (G' : G.Subgraph) (h : G'.IsSpanning) (v : G'.verts) :
(RelIso.symm (G'.spanningCoeEquivCoeOfSpanning h)) v = v
def SimpleGraph.Subgraph.spanningCoeEquivCoeOfSpanning {V : Type u} {G : } (G' : G.Subgraph) (h : G'.IsSpanning) :
G'.spanningCoe ≃g G'.coe

spanningCoe is equivalent to coe for a subgraph that IsSpanning.

Equations
• G'.spanningCoeEquivCoeOfSpanning h = { toFun := fun (v : V) => v, , invFun := fun (v : G'.verts) => v, left_inv := , right_inv := , map_rel_iff' := }
Instances For
def SimpleGraph.Subgraph.IsInduced {V : Type u} {G : } (G' : G.Subgraph) :

A subgraph is called an induced subgraph if vertices of G' are adjacent if they are adjacent in G.

Equations
• G'.IsInduced = ∀ {v w : V}, v G'.vertsw G'.vertsG.Adj v wG'.Adj v w
Instances For
def SimpleGraph.Subgraph.support {V : Type u} {G : } (H : G.Subgraph) :
Set V

H.support is the set of vertices that form edges in the subgraph H.

Equations
Instances For
theorem SimpleGraph.Subgraph.mem_support {V : Type u} {G : } (H : G.Subgraph) {v : V} :
v H.support ∃ (w : V), H.Adj v w
theorem SimpleGraph.Subgraph.support_subset_verts {V : Type u} {G : } (H : G.Subgraph) :
H.support H.verts
def SimpleGraph.Subgraph.neighborSet {V : Type u} {G : } (G' : G.Subgraph) (v : V) :
Set V

G'.neighborSet v is the set of vertices adjacent to v in G'.

Equations
• G'.neighborSet v = {w : V | G'.Adj v w}
Instances For
theorem SimpleGraph.Subgraph.neighborSet_subset {V : Type u} {G : } (G' : G.Subgraph) (v : V) :
G'.neighborSet v G.neighborSet v
theorem SimpleGraph.Subgraph.neighborSet_subset_verts {V : Type u} {G : } (G' : G.Subgraph) (v : V) :
G'.neighborSet v G'.verts
@[simp]
theorem SimpleGraph.Subgraph.mem_neighborSet {V : Type u} {G : } (G' : G.Subgraph) (v : V) (w : V) :
w G'.neighborSet v G'.Adj v w
def SimpleGraph.Subgraph.coeNeighborSetEquiv {V : Type u} {G : } {G' : G.Subgraph} (v : G'.verts) :
(G'.coe.neighborSet v) (G'.neighborSet v)

A subgraph as a graph has equivalent neighbor sets.

Equations
• = { toFun := fun (w : (G'.coe.neighborSet v)) => w, , invFun := fun (w : (G'.neighborSet v)) => w, , , left_inv := , right_inv := }
Instances For
def SimpleGraph.Subgraph.edgeSet {V : Type u} {G : } (G' : G.Subgraph) :
Set (Sym2 V)

The edge set of G' consists of a subset of edges of G.

Equations
• G'.edgeSet =
Instances For
theorem SimpleGraph.Subgraph.edgeSet_subset {V : Type u} {G : } (G' : G.Subgraph) :
G'.edgeSet G.edgeSet
@[simp]
theorem SimpleGraph.Subgraph.mem_edgeSet {V : Type u} {G : } {G' : G.Subgraph} {v : V} {w : V} :
s(v, w) G'.edgeSet G'.Adj v w
theorem SimpleGraph.Subgraph.mem_verts_if_mem_edge {V : Type u} {G : } {G' : G.Subgraph} {e : Sym2 V} {v : V} (he : e G'.edgeSet) (hv : v e) :
v G'.verts
def SimpleGraph.Subgraph.incidenceSet {V : Type u} {G : } (G' : G.Subgraph) (v : V) :
Set (Sym2 V)

The incidenceSet is the set of edges incident to a given vertex.

Equations
Instances For
theorem SimpleGraph.Subgraph.incidenceSet_subset_incidenceSet {V : Type u} {G : } (G' : G.Subgraph) (v : V) :
G'.incidenceSet v G.incidenceSet v
theorem SimpleGraph.Subgraph.incidenceSet_subset {V : Type u} {G : } (G' : G.Subgraph) (v : V) :
G'.incidenceSet v G'.edgeSet
@[reducible, inline]
abbrev SimpleGraph.Subgraph.vert {V : Type u} {G : } (G' : G.Subgraph) (v : V) (h : v G'.verts) :
G'.verts

Give a vertex as an element of the subgraph's vertex type.

Equations
• G'.vert v h = v, h
Instances For
def SimpleGraph.Subgraph.copy {V : Type u} {G : } (G' : G.Subgraph) (V'' : Set V) (hV : V'' = G'.verts) (adj' : VVProp) (hadj : adj' = G'.Adj) :
G.Subgraph

Create an equal copy of a subgraph (see copy_eq) with possibly different definitional equalities. See Note [range copy pattern].

Equations
Instances For
theorem SimpleGraph.Subgraph.copy_eq {V : Type u} {G : } (G' : G.Subgraph) (V'' : Set V) (hV : V'' = G'.verts) (adj' : VVProp) (hadj : adj' = G'.Adj) :
instance SimpleGraph.Subgraph.instSup {V : Type u} {G : } :
Sup G.Subgraph

The union of two subgraphs.

Equations
• SimpleGraph.Subgraph.instSup = { sup := fun (G₁ G₂ : G.Subgraph) => { verts := G₁.verts G₂.verts, Adj := G₁.Adj G₂.Adj, adj_sub := , edge_vert := , symm := } }
instance SimpleGraph.Subgraph.instInf {V : Type u} {G : } :
Inf G.Subgraph

The intersection of two subgraphs.

Equations
• SimpleGraph.Subgraph.instInf = { inf := fun (G₁ G₂ : G.Subgraph) => { verts := G₁.verts G₂.verts, Adj := G₁.Adj G₂.Adj, adj_sub := , edge_vert := , symm := } }
instance SimpleGraph.Subgraph.instTop {V : Type u} {G : } :
Top G.Subgraph

The top subgraph is G as a subgraph of itself.

Equations
• SimpleGraph.Subgraph.instTop = { top := { verts := Set.univ, Adj := G.Adj, adj_sub := , edge_vert := , symm := } }
instance SimpleGraph.Subgraph.instBot {V : Type u} {G : } :
Bot G.Subgraph

The bot subgraph is the subgraph with no vertices or edges.

Equations
• SimpleGraph.Subgraph.instBot = { bot := { verts := , Adj := , adj_sub := , edge_vert := , symm := } }
instance SimpleGraph.Subgraph.instSupSet {V : Type u} {G : } :
SupSet G.Subgraph
Equations
• One or more equations did not get rendered due to their size.
instance SimpleGraph.Subgraph.instInfSet {V : Type u} {G : } :
InfSet G.Subgraph
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem SimpleGraph.Subgraph.sup_adj {V : Type u} {G : } {G₁ : G.Subgraph} {G₂ : G.Subgraph} {a : V} {b : V} :
@[simp]
theorem SimpleGraph.Subgraph.inf_adj {V : Type u} {G : } {G₁ : G.Subgraph} {G₂ : G.Subgraph} {a : V} {b : V} :
@[simp]
theorem SimpleGraph.Subgraph.top_adj {V : Type u} {G : } {a : V} {b : V} :
@[simp]
theorem SimpleGraph.Subgraph.not_bot_adj {V : Type u} {G : } {a : V} {b : V} :
@[simp]
theorem SimpleGraph.Subgraph.verts_sup {V : Type u} {G : } (G₁ : G.Subgraph) (G₂ : G.Subgraph) :
(G₁ G₂).verts = G₁.verts G₂.verts
@[simp]
theorem SimpleGraph.Subgraph.verts_inf {V : Type u} {G : } (G₁ : G.Subgraph) (G₂ : G.Subgraph) :
(G₁ G₂).verts = G₁.verts G₂.verts
@[simp]
theorem SimpleGraph.Subgraph.verts_top {V : Type u} {G : } :
.verts = Set.univ
@[simp]
theorem SimpleGraph.Subgraph.verts_bot {V : Type u} {G : } :
.verts =
@[simp]
theorem SimpleGraph.Subgraph.sSup_adj {V : Type u} {G : } {a : V} {b : V} {s : Set G.Subgraph} :
@[simp]
theorem SimpleGraph.Subgraph.sInf_adj {V : Type u} {G : } {a : V} {b : V} {s : Set G.Subgraph} :
@[simp]
theorem SimpleGraph.Subgraph.iSup_adj {ι : Sort u_1} {V : Type u} {G : } {a : V} {b : V} {f : ιG.Subgraph} :
(⨆ (i : ι), f i).Adj a b ∃ (i : ι), (f i).Adj a b
@[simp]
theorem SimpleGraph.Subgraph.iInf_adj {ι : Sort u_1} {V : Type u} {G : } {a : V} {b : V} {f : ιG.Subgraph} :
(⨅ (i : ι), f i).Adj a b (∀ (i : ι), (f i).Adj a b) G.Adj a b
theorem SimpleGraph.Subgraph.sInf_adj_of_nonempty {V : Type u} {G : } {a : V} {b : V} {s : Set G.Subgraph} (hs : s.Nonempty) :
theorem SimpleGraph.Subgraph.iInf_adj_of_nonempty {ι : Sort u_1} {V : Type u} {G : } {a : V} {b : V} [] {f : ιG.Subgraph} :
(⨅ (i : ι), f i).Adj a b ∀ (i : ι), (f i).Adj a b
@[simp]
theorem SimpleGraph.Subgraph.verts_sSup {V : Type u} {G : } (s : Set G.Subgraph) :
(sSup s).verts = G's, G'.verts
@[simp]
theorem SimpleGraph.Subgraph.verts_sInf {V : Type u} {G : } (s : Set G.Subgraph) :
(sInf s).verts = G's, G'.verts
@[simp]
theorem SimpleGraph.Subgraph.verts_iSup {ι : Sort u_1} {V : Type u} {G : } {f : ιG.Subgraph} :
(⨆ (i : ι), f i).verts = ⋃ (i : ι), (f i).verts
@[simp]
theorem SimpleGraph.Subgraph.verts_iInf {ι : Sort u_1} {V : Type u} {G : } {f : ιG.Subgraph} :
(⨅ (i : ι), f i).verts = ⋂ (i : ι), (f i).verts
theorem SimpleGraph.Subgraph.verts_spanningCoe_injective {V : Type u} {G : } :
Function.Injective fun (G' : G.Subgraph) => (G'.verts, G'.spanningCoe)
instance SimpleGraph.Subgraph.distribLattice {V : Type u} {G : } :
DistribLattice G.Subgraph

For subgraphs G₁, G₂, G₁ ≤ G₂ iff G₁.verts ⊆ G₂.verts and ∀ a b, G₁.adj a b → G₂.adj a b.

Equations
• SimpleGraph.Subgraph.distribLattice = let __src := let_fun this := Function.Injective.distribLattice (fun (G' : G.Subgraph) => (G'.verts, G'.spanningCoe)) ; this;
instance SimpleGraph.Subgraph.instBoundedOrder {V : Type u} {G : } :
BoundedOrder G.Subgraph
Equations
• SimpleGraph.Subgraph.instBoundedOrder = BoundedOrder.mk
Equations
• SimpleGraph.Subgraph.instCompletelyDistribLattice = let __src := SimpleGraph.Subgraph.distribLattice;
@[simp]
instance SimpleGraph.Subgraph.subgraphInhabited {V : Type u} {G : } :
Inhabited G.Subgraph
Equations
• SimpleGraph.Subgraph.subgraphInhabited = { default := }
@[simp]
theorem SimpleGraph.Subgraph.neighborSet_sup {V : Type u} {G : } {H : G.Subgraph} {H' : G.Subgraph} (v : V) :
(H H').neighborSet v = H.neighborSet v H'.neighborSet v
@[simp]
theorem SimpleGraph.Subgraph.neighborSet_inf {V : Type u} {G : } {H : G.Subgraph} {H' : G.Subgraph} (v : V) :
(H H').neighborSet v = H.neighborSet v H'.neighborSet v
@[simp]
theorem SimpleGraph.Subgraph.neighborSet_top {V : Type u} {G : } (v : V) :
.neighborSet v = G.neighborSet v
@[simp]
theorem SimpleGraph.Subgraph.neighborSet_bot {V : Type u} {G : } (v : V) :
.neighborSet v =
@[simp]
theorem SimpleGraph.Subgraph.neighborSet_sSup {V : Type u} {G : } (s : Set G.Subgraph) (v : V) :
(sSup s).neighborSet v = G's, G'.neighborSet v
@[simp]
theorem SimpleGraph.Subgraph.neighborSet_sInf {V : Type u} {G : } (s : Set G.Subgraph) (v : V) :
(sInf s).neighborSet v = (G's, G'.neighborSet v) G.neighborSet v
@[simp]
theorem SimpleGraph.Subgraph.neighborSet_iSup {ι : Sort u_1} {V : Type u} {G : } (f : ιG.Subgraph) (v : V) :
(⨆ (i : ι), f i).neighborSet v = ⋃ (i : ι), (f i).neighborSet v
@[simp]
theorem SimpleGraph.Subgraph.neighborSet_iInf {ι : Sort u_1} {V : Type u} {G : } (f : ιG.Subgraph) (v : V) :
(⨅ (i : ι), f i).neighborSet v = (⋂ (i : ι), (f i).neighborSet v) G.neighborSet v
@[simp]
theorem SimpleGraph.Subgraph.edgeSet_top {V : Type u} {G : } :
.edgeSet = G.edgeSet
@[simp]
theorem SimpleGraph.Subgraph.edgeSet_bot {V : Type u} {G : } :
.edgeSet =
@[simp]
theorem SimpleGraph.Subgraph.edgeSet_inf {V : Type u} {G : } {H₁ : G.Subgraph} {H₂ : G.Subgraph} :
(H₁ H₂).edgeSet = H₁.edgeSet H₂.edgeSet
@[simp]
theorem SimpleGraph.Subgraph.edgeSet_sup {V : Type u} {G : } {H₁ : G.Subgraph} {H₂ : G.Subgraph} :
(H₁ H₂).edgeSet = H₁.edgeSet H₂.edgeSet
@[simp]
theorem SimpleGraph.Subgraph.edgeSet_sSup {V : Type u} {G : } (s : Set G.Subgraph) :
(sSup s).edgeSet = G's, G'.edgeSet
@[simp]
theorem SimpleGraph.Subgraph.edgeSet_sInf {V : Type u} {G : } (s : Set G.Subgraph) :
(sInf s).edgeSet = (G's, G'.edgeSet) G.edgeSet
@[simp]
theorem SimpleGraph.Subgraph.edgeSet_iSup {ι : Sort u_1} {V : Type u} {G : } (f : ιG.Subgraph) :
(⨆ (i : ι), f i).edgeSet = ⋃ (i : ι), (f i).edgeSet
@[simp]
theorem SimpleGraph.Subgraph.edgeSet_iInf {ι : Sort u_1} {V : Type u} {G : } (f : ιG.Subgraph) :
(⨅ (i : ι), f i).edgeSet = (⋂ (i : ι), (f i).edgeSet) G.edgeSet
@[simp]
theorem SimpleGraph.Subgraph.spanningCoe_top {V : Type u} {G : } :
.spanningCoe = G
@[simp]
theorem SimpleGraph.Subgraph.spanningCoe_bot {V : Type u} {G : } :
.spanningCoe =
@[simp]
theorem SimpleGraph.toSubgraph_adj {V : Type u} {G : } (H : ) (h : H G) :
∀ (a a_1 : V), ().Adj a a_1 = H.Adj a a_1
@[simp]
theorem SimpleGraph.toSubgraph_verts {V : Type u} {G : } (H : ) (h : H G) :
().verts = Set.univ
def SimpleGraph.toSubgraph {V : Type u} {G : } (H : ) (h : H G) :
G.Subgraph

Turn a subgraph of a SimpleGraph into a member of its subgraph type.

Equations
• = { verts := Set.univ, Adj := H.Adj, adj_sub := , edge_vert := , symm := }
Instances For
theorem SimpleGraph.Subgraph.support_mono {V : Type u} {G : } {H : G.Subgraph} {H' : G.Subgraph} (h : H H') :
H.support H'.support
theorem SimpleGraph.toSubgraph.isSpanning {V : Type u} {G : } (H : ) (h : H G) :
().IsSpanning
theorem SimpleGraph.Subgraph.spanningCoe_le_of_le {V : Type u} {G : } {H : G.Subgraph} {H' : G.Subgraph} (h : H H') :
H.spanningCoe H'.spanningCoe
def SimpleGraph.Subgraph.topEquiv {V : Type u} {G : } :
.coe ≃g G

The top of the Subgraph G lattice is equivalent to the graph itself.

Equations
• SimpleGraph.Subgraph.topEquiv = { toFun := fun (v : .verts) => v, invFun := fun (v : V) => v, trivial, left_inv := , right_inv := , map_rel_iff' := }
Instances For

The bottom of the Subgraph G lattice is equivalent to the empty graph on the empty vertex type.

Equations
• SimpleGraph.Subgraph.botEquiv = { toFun := fun (v : .verts) => , invFun := fun (v : Empty) => v.elim, left_inv := , right_inv := , map_rel_iff' := }
Instances For
theorem SimpleGraph.Subgraph.edgeSet_mono {V : Type u} {G : } {H₁ : G.Subgraph} {H₂ : G.Subgraph} (h : H₁ H₂) :
H₁.edgeSet H₂.edgeSet
theorem Disjoint.edgeSet {V : Type u} {G : } {H₁ : G.Subgraph} {H₂ : G.Subgraph} (h : Disjoint H₁ H₂) :
Disjoint H₁.edgeSet H₂.edgeSet
@[simp]
theorem SimpleGraph.Subgraph.map_verts {V : Type u} {W : Type v} {G : } {G' : } (f : G →g G') (H : G.Subgraph) :
().verts = f '' H.verts
@[simp]
theorem SimpleGraph.Subgraph.map_adj {V : Type u} {W : Type v} {G : } {G' : } (f : G →g G') (H : G.Subgraph) :
∀ (a a_1 : W), ().Adj a a_1 = Relation.Map H.Adj (f) (f) a a_1
def SimpleGraph.Subgraph.map {V : Type u} {W : Type v} {G : } {G' : } (f : G →g G') (H : G.Subgraph) :
G'.Subgraph

Graph homomorphisms induce a covariant function on subgraphs.

Equations
• = { verts := f '' H.verts, Adj := Relation.Map H.Adj f f, adj_sub := , edge_vert := , symm := }
Instances For
theorem SimpleGraph.Subgraph.map_monotone {V : Type u} {W : Type v} {G : } {G' : } (f : G →g G') :
theorem SimpleGraph.Subgraph.map_sup {V : Type u} {W : Type v} {G : } {G' : } (f : G →g G') {H : G.Subgraph} {H' : G.Subgraph} :
@[simp]
theorem SimpleGraph.Subgraph.comap_adj {V : Type u} {W : Type v} {G : } {G' : } (f : G →g G') (H : G'.Subgraph) (u : V) (v : V) :
@[simp]
theorem SimpleGraph.Subgraph.comap_verts {V : Type u} {W : Type v} {G : } {G' : } (f : G →g G') (H : G'.Subgraph) :
.verts = f ⁻¹' H.verts
def SimpleGraph.Subgraph.comap {V : Type u} {W : Type v} {G : } {G' : } (f : G →g G') (H : G'.Subgraph) :
G.Subgraph

Graph homomorphisms induce a contravariant function on subgraphs.

Equations
• = { verts := f ⁻¹' H.verts, Adj := fun (u v : V) => G.Adj u v H.Adj (f u) (f v), adj_sub := , edge_vert := , symm := }
Instances For
theorem SimpleGraph.Subgraph.comap_monotone {V : Type u} {W : Type v} {G : } {G' : } (f : G →g G') :
theorem SimpleGraph.Subgraph.map_le_iff_le_comap {V : Type u} {W : Type v} {G : } {G' : } (f : G →g G') (H : G.Subgraph) (H' : G'.Subgraph) :
@[simp]
theorem SimpleGraph.Subgraph.inclusion_apply_coe {V : Type u} {G : } {x : G.Subgraph} {y : G.Subgraph} (h : x y) (v : x.verts) :
() = v
def SimpleGraph.Subgraph.inclusion {V : Type u} {G : } {x : G.Subgraph} {y : G.Subgraph} (h : x y) :
x.coe →g y.coe

Given two subgraphs, one a subgraph of the other, there is an induced injective homomorphism of the subgraphs as graphs.

Equations
• = { toFun := fun (v : x.verts) => v, , map_rel' := }
Instances For
theorem SimpleGraph.Subgraph.inclusion.injective {V : Type u} {G : } {x : G.Subgraph} {y : G.Subgraph} (h : x y) :
@[simp]
theorem SimpleGraph.Subgraph.hom_apply {V : Type u} {G : } (x : G.Subgraph) (v : x.verts) :
x.hom v = v
def SimpleGraph.Subgraph.hom {V : Type u} {G : } (x : G.Subgraph) :
x.coe →g G

There is an induced injective homomorphism of a subgraph of G into G.

Equations
• x.hom = { toFun := fun (v : x.verts) => v, map_rel' := }
Instances For
@[simp]
theorem SimpleGraph.Subgraph.coe_hom {V : Type u} {G : } (x : G.Subgraph) :
x.hom = fun (v : x.verts) => v
theorem SimpleGraph.Subgraph.hom.injective {V : Type u} {G : } {x : G.Subgraph} :
@[simp]
theorem SimpleGraph.Subgraph.spanningHom_apply {V : Type u} {G : } (x : G.Subgraph) (a : V) :
x.spanningHom a = id a
def SimpleGraph.Subgraph.spanningHom {V : Type u} {G : } (x : G.Subgraph) :
x.spanningCoe →g G

There is an induced injective homomorphism of a subgraph of G as a spanning subgraph into G.

Equations
• x.spanningHom = { toFun := id, map_rel' := }
Instances For
theorem SimpleGraph.Subgraph.spanningHom.injective {V : Type u} {G : } {x : G.Subgraph} :
Function.Injective x.spanningHom
theorem SimpleGraph.Subgraph.neighborSet_subset_of_subgraph {V : Type u} {G : } {x : G.Subgraph} {y : G.Subgraph} (h : x y) (v : V) :
x.neighborSet v y.neighborSet v
instance SimpleGraph.Subgraph.neighborSet.decidablePred {V : Type u} {G : } (G' : G.Subgraph) [h : DecidableRel G'.Adj] (v : V) :
DecidablePred fun (x : V) => x G'.neighborSet v
Equations
instance SimpleGraph.Subgraph.finiteAt {V : Type u} {G : } {G' : G.Subgraph} (v : G'.verts) [DecidableRel G'.Adj] [Fintype (G.neighborSet v)] :
Fintype (G'.neighborSet v)

If a graph is locally finite at a vertex, then so is a subgraph of that graph.

Equations
• = (G.neighborSet v).fintypeSubset
def SimpleGraph.Subgraph.finiteAtOfSubgraph {V : Type u} {G : } {G' : G.Subgraph} {G'' : G.Subgraph} [DecidableRel G'.Adj] (h : G' G'') (v : G'.verts) [Fintype (G''.neighborSet v)] :
Fintype (G'.neighborSet v)

If a subgraph is locally finite at a vertex, then so are subgraphs of that subgraph.

This is not an instance because G'' cannot be inferred.

Equations
• = (G''.neighborSet v).fintypeSubset
Instances For
instance SimpleGraph.Subgraph.instFintypeElemNeighborSetOfVertsOfDecidablePredMemSet {V : Type u} {G : } (G' : G.Subgraph) [Fintype G'.verts] (v : V) [DecidablePred fun (x : V) => x G'.neighborSet v] :
Fintype (G'.neighborSet v)
Equations
• G'.instFintypeElemNeighborSetOfVertsOfDecidablePredMemSet v = G'.verts.fintypeSubset
instance SimpleGraph.Subgraph.coeFiniteAt {V : Type u} {G : } {G' : G.Subgraph} (v : G'.verts) [Fintype (G'.neighborSet v)] :
Fintype (G'.coe.neighborSet v)
Equations
theorem SimpleGraph.Subgraph.IsSpanning.card_verts {V : Type u} {G : } [] {G' : G.Subgraph} [Fintype G'.verts] (h : G'.IsSpanning) :
G'.verts.toFinset.card =
def SimpleGraph.Subgraph.degree {V : Type u} {G : } (G' : G.Subgraph) (v : V) [Fintype (G'.neighborSet v)] :

The degree of a vertex in a subgraph. It's zero for vertices outside the subgraph.

Equations
Instances For
theorem SimpleGraph.Subgraph.finset_card_neighborSet_eq_degree {V : Type u} {G : } {G' : G.Subgraph} {v : V} [Fintype (G'.neighborSet v)] :
(G'.neighborSet v).toFinset.card = G'.degree v
theorem SimpleGraph.Subgraph.degree_le {V : Type u} {G : } (G' : G.Subgraph) (v : V) [Fintype (G'.neighborSet v)] [Fintype (G.neighborSet v)] :
G'.degree v G.degree v
theorem SimpleGraph.Subgraph.degree_le' {V : Type u} {G : } (G' : G.Subgraph) (G'' : G.Subgraph) (h : G' G'') (v : V) [Fintype (G'.neighborSet v)] [Fintype (G''.neighborSet v)] :
G'.degree v G''.degree v
@[simp]
theorem SimpleGraph.Subgraph.coe_degree {V : Type u} {G : } (G' : G.Subgraph) (v : G'.verts) [Fintype (G'.coe.neighborSet v)] [Fintype (G'.neighborSet v)] :
G'.coe.degree v = G'.degree v
@[simp]
theorem SimpleGraph.Subgraph.degree_spanningCoe {V : Type u} {G : } {G' : G.Subgraph} (v : V) [Fintype (G'.neighborSet v)] [Fintype (G'.spanningCoe.neighborSet v)] :
G'.spanningCoe.degree v = G'.degree v
theorem SimpleGraph.Subgraph.degree_eq_one_iff_unique_adj {V : Type u} {G : } {G' : G.Subgraph} {v : V} [Fintype (G'.neighborSet v)] :
G'.degree v = 1 ∃! w : V, G'.Adj v w

### Properties of singletonSubgraph and subgraphOfAdj#

instance SimpleGraph.nonempty_singletonSubgraph_verts {V : Type u} {G : } (v : V) :
Nonempty (G.singletonSubgraph v).verts
Equations
• =
@[simp]
theorem SimpleGraph.singletonSubgraph_le_iff {V : Type u} {G : } (v : V) (H : G.Subgraph) :
G.singletonSubgraph v H v H.verts
@[simp]
theorem SimpleGraph.map_singletonSubgraph {V : Type u} {W : Type v} {G : } {G' : } (f : G →g G') {v : V} :
SimpleGraph.Subgraph.map f (G.singletonSubgraph v) = G'.singletonSubgraph (f v)
@[simp]
theorem SimpleGraph.neighborSet_singletonSubgraph {V : Type u} {G : } (v : V) (w : V) :
(G.singletonSubgraph v).neighborSet w =
@[simp]
theorem SimpleGraph.edgeSet_singletonSubgraph {V : Type u} {G : } (v : V) :
(G.singletonSubgraph v).edgeSet =
theorem SimpleGraph.eq_singletonSubgraph_iff_verts_eq {V : Type u} {G : } (H : G.Subgraph) {v : V} :
H = G.singletonSubgraph v H.verts = {v}
instance SimpleGraph.nonempty_subgraphOfAdj_verts {V : Type u} {G : } {v : V} {w : V} (hvw : G.Adj v w) :
Equations
• =
@[simp]
theorem SimpleGraph.edgeSet_subgraphOfAdj {V : Type u} {G : } {v : V} {w : V} (hvw : G.Adj v w) :
theorem SimpleGraph.subgraphOfAdj_le_of_adj {V : Type u} {G : } {v : V} {w : V} (H : G.Subgraph) (h : H.Adj v w) :
theorem SimpleGraph.subgraphOfAdj_symm {V : Type u} {G : } {v : V} {w : V} (hvw : G.Adj v w) :
@[simp]
theorem SimpleGraph.map_subgraphOfAdj {V : Type u} {W : Type v} {G : } {G' : } (f : G →g G') {v : V} {w : V} (hvw : G.Adj v w) :
theorem SimpleGraph.neighborSet_subgraphOfAdj_subset {V : Type u} {G : } {u : V} {v : V} {w : V} (hvw : G.Adj v w) :
@[simp]
theorem SimpleGraph.neighborSet_fst_subgraphOfAdj {V : Type u} {G : } {v : V} {w : V} (hvw : G.Adj v w) :
@[simp]
theorem SimpleGraph.neighborSet_snd_subgraphOfAdj {V : Type u} {G : } {v : V} {w : V} (hvw : G.Adj v w) :
@[simp]
theorem SimpleGraph.neighborSet_subgraphOfAdj_of_ne_of_ne {V : Type u} {G : } {u : V} {v : V} {w : V} (hvw : G.Adj v w) (hv : u v) (hw : u w) :
theorem SimpleGraph.neighborSet_subgraphOfAdj {V : Type u} {G : } [] {u : V} {v : V} {w : V} (hvw : G.Adj v w) :
(G.subgraphOfAdj hvw).neighborSet u = (if u = v then {w} else ) if u = w then {v} else
theorem SimpleGraph.singletonSubgraph_fst_le_subgraphOfAdj {V : Type u} {G : } {u : V} {v : V} {h : G.Adj u v} :
theorem SimpleGraph.singletonSubgraph_snd_le_subgraphOfAdj {V : Type u} {G : } {u : V} {v : V} {h : G.Adj u v} :

### Subgraphs of subgraphs #

@[reducible, inline]
abbrev SimpleGraph.Subgraph.coeSubgraph {V : Type u} {G : } {G' : G.Subgraph} :
G'.coe.SubgraphG.Subgraph

Given a subgraph of a subgraph of G, construct a subgraph of G.

Equations
Instances For
@[reducible, inline]
abbrev SimpleGraph.Subgraph.restrict {V : Type u} {G : } {G' : G.Subgraph} :
G.SubgraphG'.coe.Subgraph

Given a subgraph of G, restrict it to being a subgraph of another subgraph G' by taking the portion of G that intersects G'.

Equations
• SimpleGraph.Subgraph.restrict =
Instances For
theorem SimpleGraph.Subgraph.coeSubgraph_adj {V : Type u} {G : } {G' : G.Subgraph} (G'' : G'.coe.Subgraph) (v : V) (w : V) :
.Adj v w ∃ (hv : v G'.verts) (hw : w G'.verts), G''.Adj v, hv w, hw
theorem SimpleGraph.Subgraph.restrict_adj {V : Type u} {G : } {G' : G.Subgraph} {G'' : G.Subgraph} (v : G'.verts) (w : G'.verts) :
theorem SimpleGraph.Subgraph.restrict_coeSubgraph {V : Type u} {G : } {G' : G.Subgraph} (G'' : G'.coe.Subgraph) :
theorem SimpleGraph.Subgraph.coeSubgraph_injective {V : Type u} {G : } (G' : G.Subgraph) :
Function.Injective SimpleGraph.Subgraph.coeSubgraph
theorem SimpleGraph.Subgraph.coeSubgraph_le {V : Type u} {G : } {H : G.Subgraph} (H' : H.coe.Subgraph) :
theorem SimpleGraph.Subgraph.coeSubgraph_restrict_eq {V : Type u} {G : } {H : G.Subgraph} (H' : G.Subgraph) :

### Edge deletion #

def SimpleGraph.Subgraph.deleteEdges {V : Type u} {G : } (G' : G.Subgraph) (s : Set (Sym2 V)) :
G.Subgraph

Given a subgraph G' and a set of vertex pairs, remove all of the corresponding edges from its edge set, if present.

Equations
• G'.deleteEdges s = { verts := G'.verts, Adj := G'.Adj \ , adj_sub := , edge_vert := , symm := }
Instances For
@[simp]
theorem SimpleGraph.Subgraph.deleteEdges_verts {V : Type u} {G : } {G' : G.Subgraph} (s : Set (Sym2 V)) :
(G'.deleteEdges s).verts = G'.verts
@[simp]
theorem SimpleGraph.Subgraph.deleteEdges_adj {V : Type u} {G : } {G' : G.Subgraph} (s : Set (Sym2 V)) (v : V) (w : V) :
@[simp]
theorem SimpleGraph.Subgraph.deleteEdges_deleteEdges {V : Type u} {G : } {G' : G.Subgraph} (s : Set (Sym2 V)) (s' : Set (Sym2 V)) :
(G'.deleteEdges s).deleteEdges s' = G'.deleteEdges (s s')
@[simp]
theorem SimpleGraph.Subgraph.deleteEdges_empty_eq {V : Type u} {G : } {G' : G.Subgraph} :
G'.deleteEdges = G'
@[simp]
theorem SimpleGraph.Subgraph.deleteEdges_spanningCoe_eq {V : Type u} {G : } {G' : G.Subgraph} (s : Set (Sym2 V)) :
G'.spanningCoe.deleteEdges s = (G'.deleteEdges s).spanningCoe
theorem SimpleGraph.Subgraph.deleteEdges_coe_eq {V : Type u} {G : } {G' : G.Subgraph} (s : Set (Sym2 G'.verts)) :
G'.coe.deleteEdges s = (G'.deleteEdges (Sym2.map Subtype.val '' s)).coe
theorem SimpleGraph.Subgraph.coe_deleteEdges_eq {V : Type u} {G : } {G' : G.Subgraph} (s : Set (Sym2 V)) :
(G'.deleteEdges s).coe = G'.coe.deleteEdges (Sym2.map Subtype.val ⁻¹' s)
theorem SimpleGraph.Subgraph.deleteEdges_le {V : Type u} {G : } {G' : G.Subgraph} (s : Set (Sym2 V)) :
G'.deleteEdges s G'
theorem SimpleGraph.Subgraph.deleteEdges_le_of_le {V : Type u} {G : } {G' : G.Subgraph} {s : Set (Sym2 V)} {s' : Set (Sym2 V)} (h : s s') :
G'.deleteEdges s' G'.deleteEdges s
@[simp]
theorem SimpleGraph.Subgraph.deleteEdges_inter_edgeSet_left_eq {V : Type u} {G : } {G' : G.Subgraph} (s : Set (Sym2 V)) :
G'.deleteEdges (G'.edgeSet s) = G'.deleteEdges s
@[simp]
theorem SimpleGraph.Subgraph.deleteEdges_inter_edgeSet_right_eq {V : Type u} {G : } {G' : G.Subgraph} (s : Set (Sym2 V)) :
G'.deleteEdges (s G'.edgeSet) = G'.deleteEdges s
theorem SimpleGraph.Subgraph.coe_deleteEdges_le {V : Type u} {G : } {G' : G.Subgraph} (s : Set (Sym2 V)) :
(G'.deleteEdges s).coe G'.coe
theorem SimpleGraph.Subgraph.spanningCoe_deleteEdges_le {V : Type u} {G : } (G' : G.Subgraph) (s : Set (Sym2 V)) :
(G'.deleteEdges s).spanningCoe G'.spanningCoe

### Induced subgraphs #

@[simp]
theorem SimpleGraph.Subgraph.induce_verts {V : Type u} {G : } (G' : G.Subgraph) (s : Set V) :
(G'.induce s).verts = s
@[simp]
theorem SimpleGraph.Subgraph.induce_adj {V : Type u} {G : } (G' : G.Subgraph) (s : Set V) (u : V) (v : V) :
(G'.induce s).Adj u v = (u s v s G'.Adj u v)
def SimpleGraph.Subgraph.induce {V : Type u} {G : } (G' : G.Subgraph) (s : Set V) :
G.Subgraph

The induced subgraph of a subgraph. The expectation is that s ⊆ G'.verts for the usual notion of an induced subgraph, but, in general, s is taken to be the new vertex set and edges are induced from the subgraph G'.

Equations
• G'.induce s = { verts := s, Adj := fun (u v : V) => u s v s G'.Adj u v, adj_sub := , edge_vert := , symm := }
Instances For
theorem SimpleGraph.induce_eq_coe_induce_top {V : Type u} {G : } (s : Set V) :
= (.induce s).coe
theorem SimpleGraph.Subgraph.induce_mono {V : Type u} {G : } {G' : G.Subgraph} {G'' : G.Subgraph} {s : Set V} {s' : Set V} (hg : G' G'') (hs : s s') :
G'.induce s G''.induce s'
theorem SimpleGraph.Subgraph.induce_mono_left {V : Type u} {G : } {G' : G.Subgraph} {G'' : G.Subgraph} {s : Set V} (hg : G' G'') :
G'.induce s G''.induce s
theorem SimpleGraph.Subgraph.induce_mono_right {V : Type u} {G : } {G' : G.Subgraph} {s : Set V} {s' : Set V} (hs : s s') :
G'.induce s G'.induce s'
@[simp]
theorem SimpleGraph.Subgraph.induce_empty {V : Type u} {G : } {G' : G.Subgraph} :
G'.induce =
@[simp]
theorem SimpleGraph.Subgraph.induce_self_verts {V : Type u} {G : } {G' : G.Subgraph} :
G'.induce G'.verts = G'
theorem SimpleGraph.Subgraph.le_induce_top_verts {V : Type u} {G : } {G' : G.Subgraph} :
G' .induce G'.verts
theorem SimpleGraph.Subgraph.le_induce_union {V : Type u} {G : } {G' : G.Subgraph} {s : Set V} {s' : Set V} :
G'.induce s G'.induce s' G'.induce (s s')
theorem SimpleGraph.Subgraph.le_induce_union_left {V : Type u} {G : } {G' : G.Subgraph} {s : Set V} {s' : Set V} :
G'.induce s G'.induce (s s')
theorem SimpleGraph.Subgraph.le_induce_union_right {V : Type u} {G : } {G' : G.Subgraph} {s : Set V} {s' : Set V} :
G'.induce s' G'.induce (s s')
theorem SimpleGraph.Subgraph.singletonSubgraph_eq_induce {V : Type u} {G : } {v : V} :
G.singletonSubgraph v = .induce {v}
theorem SimpleGraph.Subgraph.subgraphOfAdj_eq_induce {V : Type u} {G : } {v : V} {w : V} (hvw : G.Adj v w) :
G.subgraphOfAdj hvw = .induce {v, w}
@[reducible, inline]
abbrev SimpleGraph.Subgraph.deleteVerts {V : Type u} {G : } (G' : G.Subgraph) (s : Set V) :
G.Subgraph

Given a subgraph and a set of vertices, delete all the vertices from the subgraph, if present. Any edges incident to the deleted vertices are deleted as well.

Equations
• G'.deleteVerts s = G'.induce (G'.verts \ s)
Instances For
theorem SimpleGraph.Subgraph.deleteVerts_verts {V : Type u} {G : } {G' : G.Subgraph} {s : Set V} :
(G'.deleteVerts s).verts = G'.verts \ s
theorem SimpleGraph.Subgraph.deleteVerts_adj {V : Type u} {G : } {G' : G.Subgraph} {s : Set V} {u : V} {v : V} :
(G'.deleteVerts s).Adj u v u G'.verts us v G'.verts vs G'.Adj u v
@[simp]
theorem SimpleGraph.Subgraph.deleteVerts_deleteVerts {V : Type u} {G : } {G' : G.Subgraph} (s : Set V) (s' : Set V) :
(G'.deleteVerts s).deleteVerts s' = G'.deleteVerts (s s')
@[simp]
theorem SimpleGraph.Subgraph.deleteVerts_empty {V : Type u} {G : } {G' : G.Subgraph} :
G'.deleteVerts = G'
theorem SimpleGraph.Subgraph.deleteVerts_le {V : Type u} {G : } {G' : G.Subgraph} {s : Set V} :
G'.deleteVerts s G'
theorem SimpleGraph.Subgraph.deleteVerts_mono {V : Type u} {G : } {s : Set V} {G' : G.Subgraph} {G'' : G.Subgraph} (h : G' G'') :
G'.deleteVerts s G''.deleteVerts s
theorem SimpleGraph.Subgraph.deleteVerts_anti {V : Type u} {G : } {G' : G.Subgraph} {s : Set V} {s' : Set V} (h : s s') :
G'.deleteVerts s' G'.deleteVerts s
@[simp]
theorem SimpleGraph.Subgraph.deleteVerts_inter_verts_left_eq {V : Type u} {G : } {G' : G.Subgraph} {s : Set V} :
G'.deleteVerts (G'.verts s) = G'.deleteVerts s
@[simp]
theorem SimpleGraph.Subgraph.deleteVerts_inter_verts_set_right_eq {V : Type u} {G : } {G' : G.Subgraph} {s : Set V} :
G'.deleteVerts (s G'.verts) = G'.deleteVerts s