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

• A bounded_lattice (subgraph G) instance, under the subgraph relation.

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

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) :
theorem simple_graph.subgraph.adj_comm {V : Type u} {G : simple_graph V} (G' : G.subgraph) (v w : V) :
theorem simple_graph.subgraph.adj_symm {V : Type u} {G : simple_graph V} (G' : G.subgraph) {u v : V} (h : G'.adj u v) :
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) :
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.spanning_coe_adj_sub {V : Type u} {G : simple_graph V} (H : G.subgraph) (u v : (H.verts)) (h : H.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.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
theorem simple_graph.subgraph.neighbor_set_subset {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) :
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
@[instance]
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
@[instance]
Equations
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.to_subgraph.is_spanning {V : Type u} {G : simple_graph V} (H : simple_graph V) (h : H G) :
theorem simple_graph.subgraph.spanning_coe.is_subgraph_of_is_subgraph {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
def simple_graph.subgraph.map {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.map.injective {V : Type u} {G : simple_graph V} {x y : G.subgraph} (h : x y) :
def simple_graph.subgraph.map_top {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.map_top.injective {V : Type u} {G : simple_graph V} {x : G.subgraph} :
@[simp]
theorem simple_graph.subgraph.map_top_to_fun {V : Type u} {G : simple_graph V} {x : G.subgraph} (v : (x.verts)) :
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) :
@[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
@[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
@[instance]
Equations
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. Is 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