# mathlibdocumentation

combinatorics.simple_graph.subgraph

# 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.

## Main definitions #

• subgraph G is the type of subgraphs of a G : simple_graph

• subgraph.neighbor_set, subgraph.incidence_set, and subgraph.degree are like their simple_graph counterparts, but they refer to vertices from G to avoid subtype coercions.

• subgraph.coe is the coercion from a G' : subgraph G to a simple_graph G'.verts. (This cannot be a has_coe instance since the destination type depends on G'.)

• subgraph.is_spanning for whether a subgraph is a spanning subgraph and subgraph.is_induced for whether a subgraph is an induced subgraph.

• Instances for lattice (subgraph G) and bounded_order (subgraph G).

• simple_graph.to_subgraph: If a simple_graph is a subgraph of another, then you can turn it into a member of the larger graph's simple_graph.subgraph type.

• Graph homomorphisms from a subgraph to a graph (subgraph.map_top) and between subgraphs (subgraph.map).

## Implementation notes #

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

## Todo #

• Images of graph homomorphisms as subgraphs.
@[ext]
structure simple_graph.subgraph {V : Type u} (G : simple_graph V) :
Type u
• verts : set V
• adj : V → V → Prop
• edge_vert : ∀ {v w : V}, self.adj v wv self.verts
• symm : symmetric self.adj . "obviously"

A subgraph of a simple_graph 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.

Instances for simple_graph.subgraph
theorem simple_graph.subgraph.ext {V : Type u} {G : simple_graph V} (x y : G.subgraph) (h : x.verts = y.verts) (h_1 : x.adj = y.adj) :
x = y
theorem simple_graph.subgraph.ext_iff {V : Type u} {G : simple_graph V} (x y : G.subgraph) :
@[protected]
theorem simple_graph.subgraph.loopless {V : Type u} {G : simple_graph V} (G' : G.subgraph) :
theorem simple_graph.subgraph.adj_comm {V : Type u} {G : simple_graph V} (G' : G.subgraph) (v w : V) :
@[symm]
theorem simple_graph.subgraph.adj_symm {V : Type u} {G : simple_graph V} (G' : G.subgraph) {u v : V} (h : G'.adj u v) :
@[protected]
theorem simple_graph.subgraph.adj.symm {V : Type u} {G : simple_graph V} {G' : G.subgraph} {u v : V} (h : G'.adj u v) :
@[protected]
def simple_graph.subgraph.coe {V : Type u} {G : simple_graph V} (G' : G.subgraph) :

Coercion from G' : subgraph G to a simple_graph ↥G'.verts.

Equations
@[simp]
theorem simple_graph.subgraph.coe_adj {V : Type u} {G : simple_graph V} (G' : G.subgraph) (v w : (G'.verts)) :
@[simp]
theorem simple_graph.subgraph.coe_adj_sub {V : Type u} {G : simple_graph V} (G' : G.subgraph) (u v : (G'.verts)) (h : G'.coe.adj u v) :
def simple_graph.subgraph.is_spanning {V : Type u} {G : simple_graph V} (G' : G.subgraph) :
Prop

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

Equations
@[simp]
theorem simple_graph.subgraph.spanning_coe_adj {V : Type u} {G : simple_graph V} (G' : G.subgraph) (ᾰ ᾰ_1 : V) :
@[protected]
def simple_graph.subgraph.spanning_coe {V : Type u} {G : simple_graph V} (G' : G.subgraph) :

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

Equations
@[simp]
theorem simple_graph.subgraph.adj.of_spanning_coe {V : Type u} {G : simple_graph V} {G' : G.subgraph} {u v : (G'.verts)} (h : G'.spanning_coe.adj u v) :
@[simp]
theorem simple_graph.subgraph.spanning_coe_equiv_coe_of_spanning_apply_coe {V : Type u} {G : simple_graph V} (G' : G.subgraph) (h : G'.is_spanning) (v : V) :
v) = v

spanning_coe is equivalent to coe for a subgraph that is_spanning.

Equations
@[simp]
def simple_graph.subgraph.is_induced {V : Type u} {G : simple_graph V} (G' : G.subgraph) :
Prop

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

Equations
def simple_graph.subgraph.support {V : Type u} {G : simple_graph V} (H : G.subgraph) :
set V

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

Equations
theorem simple_graph.subgraph.mem_support {V : Type u} {G : simple_graph V} (H : G.subgraph) {v : V} :
v H.support ∃ (w : V), H.adj v w
def simple_graph.subgraph.neighbor_set {V : Type u} {G : simple_graph V} (G' : G.subgraph) (v : V) :
set V

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

Equations
Instances for ↥simple_graph.subgraph.neighbor_set
theorem simple_graph.subgraph.neighbor_set_subset {V : Type u} {G : simple_graph V} (G' : G.subgraph) (v : V) :
theorem simple_graph.subgraph.neighbor_set_subset_verts {V : Type u} {G : simple_graph V} (G' : G.subgraph) (v : V) :
@[simp]
theorem simple_graph.subgraph.mem_neighbor_set {V : Type u} {G : simple_graph V} (G' : G.subgraph) (v w : V) :
w G'.neighbor_set v G'.adj v w

A subgraph as a graph has equivalent neighbor sets.

Equations
def simple_graph.subgraph.edge_set {V : Type u} {G : simple_graph V} (G' : G.subgraph) :
set (sym2 V)

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

Equations
@[simp]
theorem simple_graph.subgraph.mem_edge_set {V : Type u} {G : simple_graph V} {G' : G.subgraph} {v w : V} :
(v, w) G'.edge_set G'.adj v w
theorem simple_graph.subgraph.mem_verts_if_mem_edge {V : Type u} {G : simple_graph V} {G' : G.subgraph} {e : sym2 V} {v : V} (he : e G'.edge_set) (hv : v e) :
v G'.verts
def simple_graph.subgraph.incidence_set {V : Type u} {G : simple_graph V} (G' : G.subgraph) (v : V) :
set (sym2 V)

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

Equations
theorem simple_graph.subgraph.incidence_set_subset {V : Type u} {G : simple_graph V} (G' : G.subgraph) (v : V) :
@[reducible]
def simple_graph.subgraph.vert {V : Type u} {G : simple_graph V} (G' : G.subgraph) (v : V) (h : v G'.verts) :

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

Equations
def simple_graph.subgraph.copy {V : Type u} {G : simple_graph V} (G' : G.subgraph) (V'' : set V) (hV : V'' = G'.verts) (adj' : V → V → Prop) (hadj : adj' = G'.adj) :

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

Equations
theorem simple_graph.subgraph.copy_eq {V : Type u} {G : simple_graph V} (G' : G.subgraph) (V'' : set V) (hV : V'' = G'.verts) (adj' : V → V → Prop) (hadj : adj' = G'.adj) :
def simple_graph.subgraph.union {V : Type u} {G : simple_graph V} (x y : G.subgraph) :

The union of two subgraphs.

Equations
def simple_graph.subgraph.inter {V : Type u} {G : simple_graph V} (x y : G.subgraph) :

The intersection of two subgraphs.

Equations
def simple_graph.subgraph.top {V : Type u} {G : simple_graph V} :

The top subgraph is G as a subgraph of itself.

Equations
def simple_graph.subgraph.bot {V : Type u} {G : simple_graph V} :

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

Equations
def simple_graph.subgraph.is_subgraph {V : Type u} {G : simple_graph V} (x y : G.subgraph) :
Prop

The relation that one subgraph is a subgraph of another.

Equations
@[protected, instance]
def simple_graph.subgraph.lattice {V : Type u} {G : simple_graph V} :
Equations
@[protected, instance]
Equations
@[simp]
@[protected, instance]
Equations
@[simp]
theorem simple_graph.subgraph.top_verts {V : Type u} {G : simple_graph V} :
@[simp]
theorem simple_graph.subgraph.top_adj_iff {V : Type u} {G : simple_graph V} {v w : V} :
@[simp]
theorem simple_graph.subgraph.bot_verts {V : Type u} {G : simple_graph V} :
@[simp]
theorem simple_graph.subgraph.not_bot_adj {V : Type u} {G : simple_graph V} {v w : V} :
@[simp]
theorem simple_graph.subgraph.inf_adj {V : Type u} {G : simple_graph V} {H₁ H₂ : G.subgraph} {v w : V} :
@[simp]
theorem simple_graph.subgraph.sup_adj {V : Type u} {G : simple_graph V} {H₁ H₂ : G.subgraph} {v w : V} :
@[simp]
theorem simple_graph.subgraph.edge_set_top {V : Type u} {G : simple_graph V} :
@[simp]
theorem simple_graph.subgraph.edge_set_bot {V : Type u} {G : simple_graph V} :
@[simp]
theorem simple_graph.subgraph.edge_set_inf {V : Type u} {G : simple_graph V} {H₁ H₂ : G.subgraph} :
(H₁ H₂).edge_set = H₁.edge_set H₂.edge_set
@[simp]
theorem simple_graph.subgraph.edge_set_sup {V : Type u} {G : simple_graph V} {H₁ H₂ : G.subgraph} :
(H₁ H₂).edge_set = H₁.edge_set H₂.edge_set
@[simp]
theorem simple_graph.subgraph.spanning_coe_top {V : Type u} {G : simple_graph V} :
@[simp]
theorem simple_graph.subgraph.spanning_coe_bot {V : Type u} {G : simple_graph V} :
def simple_graph.to_subgraph {V : Type u} {G : simple_graph V} (H : simple_graph V) (h : H G) :

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

Equations
@[simp]
theorem simple_graph.to_subgraph_adj {V : Type u} {G : simple_graph V} (H : simple_graph V) (h : H G) (ᾰ ᾰ_1 : V) :
@[simp]
theorem simple_graph.to_subgraph_verts {V : Type u} {G : simple_graph V} (H : simple_graph V) (h : H G) :
theorem simple_graph.subgraph.support_mono {V : Type u} {G : simple_graph V} {H H' : G.subgraph} (h : H H') :
theorem simple_graph.to_subgraph.is_spanning {V : Type u} {G : simple_graph V} (H : simple_graph V) (h : H G) :
theorem simple_graph.subgraph.spanning_coe_le_of_le {V : Type u} {G : simple_graph V} {H H' : G.subgraph} (h : H H') :
def simple_graph.subgraph.top_equiv {V : Type u} {G : simple_graph V} :

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

Equations
def simple_graph.subgraph.bot_equiv {V : Type u} {G : simple_graph V} :

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

Equations
theorem simple_graph.subgraph.edge_set_mono {V : Type u} {G : simple_graph V} {H₁ H₂ : G.subgraph} (h : H₁ H₂) :
theorem disjoint.edge_set {V : Type u} {G : simple_graph V} {H₁ H₂ : G.subgraph} (h : disjoint H₁ H₂) :
H₂.edge_set
@[simp]
theorem simple_graph.subgraph.map_verts {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G →g G') (H : G.subgraph) :
@[protected]
def simple_graph.subgraph.map {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G →g G') (H : G.subgraph) :

Graph homomorphisms induce a covariant function on subgraphs.

Equations
@[simp]
theorem simple_graph.subgraph.map_adj {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G →g G') (H : G.subgraph) (ᾰ ᾰ_1 : W) :
.adj ᾰ_1 = f f ᾰ_1
theorem simple_graph.subgraph.map_monotone {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G →g G') :
@[simp]
theorem simple_graph.subgraph.comap_verts {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G →g G') (H : G'.subgraph) :
@[simp]
theorem simple_graph.subgraph.comap_adj {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G →g G') (H : G'.subgraph) (u v : V) :
@[protected]
def simple_graph.subgraph.comap {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G →g G') (H : G'.subgraph) :

Graph homomorphisms induce a contravariant function on subgraphs.

Equations
theorem simple_graph.subgraph.comap_monotone {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G →g G') :
theorem simple_graph.subgraph.map_le_iff_le_comap {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G →g G') (H : G.subgraph) (H' : G'.subgraph) :
@[simp]
theorem simple_graph.subgraph.inclusion_apply_coe {V : Type u} {G : simple_graph V} {x y : G.subgraph} (h : x y) (v : (x.verts)) :
= v
def simple_graph.subgraph.inclusion {V : Type u} {G : simple_graph V} {x y : G.subgraph} (h : x y) :

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

Equations
theorem simple_graph.subgraph.inclusion.injective {V : Type u} {G : simple_graph V} {x y : G.subgraph} (h : x y) :
@[simp]
theorem simple_graph.subgraph.hom_apply {V : Type u} {G : simple_graph V} (x : G.subgraph) (v : (x.verts)) :
(x.hom) v = v
@[protected]
def simple_graph.subgraph.hom {V : Type u} {G : simple_graph V} (x : G.subgraph) :
x.coe →g G

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

Equations
theorem simple_graph.subgraph.hom.injective {V : Type u} {G : simple_graph V} {x : G.subgraph} :
def simple_graph.subgraph.spanning_hom {V : Type u} {G : simple_graph V} (x : G.subgraph) :

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

Equations
@[simp]
theorem simple_graph.subgraph.spanning_hom_apply {V : Type u} {G : simple_graph V} (x : G.subgraph) (a : V) :
theorem simple_graph.subgraph.neighbor_set_subset_of_subgraph {V : Type u} {G : simple_graph V} {x y : G.subgraph} (h : x y) (v : V) :
@[protected, instance]
def simple_graph.subgraph.neighbor_set.decidable_pred {V : Type u} {G : simple_graph V} (G' : G.subgraph) [h : decidable_rel G'.adj] (v : V) :
decidable_pred (λ (_x : V), _x G'.neighbor_set v)
Equations
@[protected, instance]

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

Equations
def simple_graph.subgraph.finite_at_of_subgraph {V : Type u} {G : simple_graph V} {G' G'' : G.subgraph} [decidable_rel G'.adj] (h : G' G'') (v : (G'.verts)) [hf : fintype (G''.neighbor_set 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
@[protected, instance]
def simple_graph.subgraph.neighbor_set.fintype {V : Type u} {G : simple_graph V} (G' : G.subgraph) [fintype (G'.verts)] (v : V) [decidable_pred (λ (_x : V), _x G'.neighbor_set v)] :
Equations
@[protected, instance]
Equations
theorem simple_graph.subgraph.is_spanning.card_verts {V : Type u} {G : simple_graph V} [fintype V] {G' : G.subgraph} [fintype (G'.verts)] (h : G'.is_spanning) :
def simple_graph.subgraph.degree {V : Type u} {G : simple_graph V} (G' : G.subgraph) (v : V) [fintype (G'.neighbor_set v)] :

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

Equations
theorem simple_graph.subgraph.degree_le {V : Type u} {G : simple_graph V} (G' : G.subgraph) (v : V) [fintype (G'.neighbor_set v)] [fintype (G.neighbor_set v)] :
G'.degree v G.degree v
theorem simple_graph.subgraph.degree_le' {V : Type u} {G : simple_graph V} (G' G'' : G.subgraph) (h : G' G'') (v : V) [fintype (G'.neighbor_set v)] [fintype (G''.neighbor_set v)] :
G'.degree v G''.degree v
@[simp]
theorem simple_graph.subgraph.coe_degree {V : Type u} {G : simple_graph V} (G' : G.subgraph) (v : (G'.verts)) [fintype (G'.coe.neighbor_set v)] [fintype (G'.neighbor_set v)] :
G'.coe.degree v = G'.degree v
@[simp]
theorem simple_graph.subgraph.degree_eq_one_iff_unique_adj {V : Type u} {G : simple_graph V} {G' : G.subgraph} {v : V} [fintype (G'.neighbor_set v)] :
G'.degree v = 1 ∃! (w : V), G'.adj v w

## Subgraphs of subgraphs #

@[protected, reducible]
def simple_graph.subgraph.coe_subgraph {V : Type u} {G : simple_graph V} {G' : G.subgraph} :

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

Equations
@[protected, reducible]
def simple_graph.subgraph.restrict {V : Type u} {G : simple_graph V} {G' : G.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
theorem simple_graph.subgraph.restrict_coe_subgraph {V : Type u} {G : simple_graph V} {G' : G.subgraph} (G'' : G'.coe.subgraph) :

## Edge deletion #

def simple_graph.subgraph.delete_edges {V : Type u} {G : simple_graph V} (G' : G.subgraph) (s : set (sym2 V)) :

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

See also: simple_graph.delete_edges.

Equations
@[simp]
theorem simple_graph.subgraph.delete_edges_verts {V : Type u} {G : simple_graph V} {G' : G.subgraph} (s : set (sym2 V)) :
@[simp]
theorem simple_graph.subgraph.delete_edges_adj {V : Type u} {G : simple_graph V} {G' : G.subgraph} (s : set (sym2 V)) (v w : V) :
@[simp]
theorem simple_graph.subgraph.delete_edges_delete_edges {V : Type u} {G : simple_graph V} {G' : G.subgraph} (s s' : set (sym2 V)) :
@[simp]
theorem simple_graph.subgraph.delete_edges_empty_eq {V : Type u} {G : simple_graph V} {G' : G.subgraph} :
= G'
@[simp]
theorem simple_graph.subgraph.delete_edges_coe_eq {V : Type u} {G : simple_graph V} {G' : G.subgraph} (s : set (sym2 (G'.verts))) :
theorem simple_graph.subgraph.coe_delete_edges_eq {V : Type u} {G : simple_graph V} {G' : G.subgraph} (s : set (sym2 V)) :
theorem simple_graph.subgraph.delete_edges_le {V : Type u} {G : simple_graph V} {G' : G.subgraph} (s : set (sym2 V)) :
theorem simple_graph.subgraph.delete_edges_le_of_le {V : Type u} {G : simple_graph V} {G' : G.subgraph} {s s' : set (sym2 V)} (h : s s') :
@[simp]
@[simp]
theorem simple_graph.subgraph.coe_delete_edges_le {V : Type u} {G : simple_graph V} {G' : G.subgraph} (s : set (sym2 V)) :

## Induced subgraphs #

def simple_graph.subgraph.induce {V : Type u} {G : simple_graph V} (G' : G.subgraph) (s : set V) :

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
@[simp]
theorem simple_graph.subgraph.induce_adj {V : Type u} {G : simple_graph V} (G' : G.subgraph) (s : set V) (u v : V) :
(G'.induce s).adj u v = (u s v s G'.adj u v)
@[simp]
theorem simple_graph.subgraph.induce_verts {V : Type u} {G : simple_graph V} (G' : G.subgraph) (s : set V) :
(G'.induce s).verts = s
theorem simple_graph.induce_eq_coe_induce_top {V : Type u} {G : simple_graph V} (s : set V) :
theorem simple_graph.subgraph.induce_mono {V : Type u} {G : simple_graph V} {G' G'' : G.subgraph} {s s' : set V} (hg : G' G'') (hs : s s') :
G'.induce s G''.induce s'
theorem simple_graph.subgraph.induce_mono_left {V : Type u} {G : simple_graph V} {G' G'' : G.subgraph} {s : set V} (hg : G' G'') :
G'.induce s G''.induce s
theorem simple_graph.subgraph.induce_mono_right {V : Type u} {G : simple_graph V} {G' : G.subgraph} {s s' : set V} (hs : s s') :
G'.induce s G'.induce s'
@[simp]
theorem simple_graph.subgraph.induce_empty {V : Type u} {G : simple_graph V} {G' : G.subgraph} :
@[simp]
theorem simple_graph.subgraph.induce_self_verts {V : Type u} {G : simple_graph V} {G' : G.subgraph} :
G'.induce G'.verts = G'
@[reducible]
def simple_graph.subgraph.delete_verts {V : Type u} {G : simple_graph V} (G' : G.subgraph) (s : set V) :

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

Equations
theorem simple_graph.subgraph.delete_verts_verts {V : Type u} {G : simple_graph V} {G' : G.subgraph} {s : set V} :
(G'.delete_verts s).verts = G'.verts \ s
theorem simple_graph.subgraph.delete_verts_adj {V : Type u} {G : simple_graph V} {G' : G.subgraph} {s : set V} {u v : V} :
(G'.delete_verts s).adj u v u G'.verts u s v G'.verts v s G'.adj u v
@[simp]
theorem simple_graph.subgraph.delete_verts_delete_verts {V : Type u} {G : simple_graph V} {G' : G.subgraph} (s s' : set V) :
@[simp]
theorem simple_graph.subgraph.delete_verts_empty {V : Type u} {G : simple_graph V} {G' : G.subgraph} :
= G'
theorem simple_graph.subgraph.delete_verts_le {V : Type u} {G : simple_graph V} {G' : G.subgraph} {s : set V} :
theorem simple_graph.subgraph.delete_verts_mono {V : Type u} {G : simple_graph V} {s : set V} {G' G'' : G.subgraph} (h : G' G'') :
theorem simple_graph.subgraph.delete_verts_anti {V : Type u} {G : simple_graph V} {G' : G.subgraph} {s s' : set V} (h : s s') :
@[simp]
theorem simple_graph.subgraph.delete_verts_inter_verts_left_eq {V : Type u} {G : simple_graph V} {G' : G.subgraph} {s : set V} :
@[simp]