mathlib documentation

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 #

Implementation notes #

Todo #

@[ext]
structure simple_graph.subgraph {V : Type u} (G : simple_graph V) :

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) :
x = y x.verts = y.verts x.adj = y.adj
@[simp]
theorem simple_graph.singleton_subgraph_adj {V : Type u} (G : simple_graph V) (v ᾰ ᾰ_1 : V) :
(G.singleton_subgraph v).adj ᾰ_1 = ᾰ_1
@[protected]
def simple_graph.singleton_subgraph {V : Type u} (G : simple_graph V) (v : V) :

The one-vertex subgraph.

Equations
@[simp]
theorem simple_graph.singleton_subgraph_verts {V : Type u} (G : simple_graph V) (v : V) :
def simple_graph.subgraph_of_adj {V : Type u} (G : simple_graph V) {v w : V} (hvw : G.adj v w) :

The one-edge subgraph.

Equations
@[simp]
theorem simple_graph.subgraph_of_adj_verts {V : Type u} (G : simple_graph V) {v w : V} (hvw : G.adj v w) :
(G.subgraph_of_adj hvw).verts = {v, w}
@[simp]
theorem simple_graph.subgraph_of_adj_adj {V : Type u} (G : simple_graph V) {v w : V} (hvw : G.adj v w) (a b : V) :
(G.subgraph_of_adj hvw).adj a b = ((v, w) = (a, b))
@[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) :
G'.adj v w G'.adj 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) :
G'.adj v u
@[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) :
G'.adj v u
@[protected]
theorem simple_graph.subgraph.adj.adj_sub {V : Type u} {G : simple_graph V} {H : G.subgraph} {u v : V} (h : H.adj u v) :
G.adj u v
@[protected]
theorem simple_graph.subgraph.adj.fst_mem {V : Type u} {G : simple_graph V} {H : G.subgraph} {u v : V} (h : H.adj u v) :
@[protected]
theorem simple_graph.subgraph.adj.snd_mem {V : Type u} {G : simple_graph V} {H : G.subgraph} {u v : V} (h : H.adj u v) :
@[protected]
theorem simple_graph.subgraph.adj.ne {V : Type u} {G : simple_graph V} {H : G.subgraph} {u v : V} (h : H.adj u v) :
u v
@[protected]

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)) :
G'.coe.adj v w = G'.adj v w
@[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) :
G.adj u v
@[protected]
theorem simple_graph.subgraph.adj.coe {V : Type u} {G : simple_graph V} {H : G.subgraph} {u v : V} (h : H.adj u v) :
H.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) :
G'.spanning_coe.adj ᾰ_1 = G'.adj ᾰ_1
@[protected]

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) :
G.adj u v

spanning_coe is equivalent to coe for a subgraph that is_spanning.

Equations
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
@[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
@[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) :
G'.copy V'' hV adj' hadj = G'
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

The top subgraph is G as a subgraph of itself.

Equations

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
@[simp]
theorem simple_graph.subgraph.top_adj_iff {V : Type u} {G : simple_graph V} {v w : V} :
.adj v w G.adj v w
@[simp]
@[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} :
(H₁ H₂).adj v w H₁.adj v w H₂.adj v w
@[simp]
theorem simple_graph.subgraph.sup_adj {V : Type u} {G : simple_graph V} {H₁ H₂ : G.subgraph} {v w : V} :
(H₁ H₂).adj v w H₁.adj v w H₂.adj v w
@[simp]
theorem simple_graph.subgraph.verts_sup {V : Type u} {G : simple_graph V} {H H' : G.subgraph} :
(H H').verts = H.verts H'.verts
@[simp]
theorem simple_graph.subgraph.verts_inf {V : Type u} {G : simple_graph V} {H H' : G.subgraph} :
(H H').verts = H.verts H'.verts
theorem simple_graph.subgraph.neighbor_set_sup {V : Type u} {G : simple_graph V} {H H' : G.subgraph} (v : V) :
theorem simple_graph.subgraph.neighbor_set_inf {V : Type u} {G : simple_graph V} {H H' : G.subgraph} (v : 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
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) :
(H.to_subgraph h).adj ᾰ_1 = H.adj ᾰ_1
@[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') :

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

Equations

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₂) :
@[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) :
(simple_graph.subgraph.map f H).adj ᾰ_1 = relation.map H.adj f f ᾰ_1
@[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) :
(simple_graph.subgraph.comap f H).adj u v = (G.adj u v H.adj (f u) (f 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
@[simp]
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
@[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

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) :
@[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
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
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

Properties of singleton_subgraph and subgraph_of_adj #

@[protected, instance]
@[simp]
theorem simple_graph.singleton_subgraph_le_iff {V : Type u} {G : simple_graph V} (v : V) (H : G.subgraph) :
@[simp]
theorem simple_graph.map_singleton_subgraph {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G →g G') {v : V} :
@[protected, instance]
def simple_graph.nonempty_subgraph_of_adj_verts {V : Type u} {G : simple_graph V} {v w : V} (hvw : G.adj v w) :
@[simp]
theorem simple_graph.edge_set_subgraph_of_adj {V : Type u} {G : simple_graph V} {v w : V} (hvw : G.adj v w) :
theorem simple_graph.subgraph_of_adj_symm {V : Type u} {G : simple_graph V} {v w : V} (hvw : G.adj v w) :
@[simp]
theorem simple_graph.map_subgraph_of_adj {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G →g G') {v w : V} (hvw : G.adj v w) :
theorem simple_graph.neighbor_set_subgraph_of_adj_subset {V : Type u} {G : simple_graph V} {u v w : V} (hvw : G.adj v w) :
@[simp]
theorem simple_graph.neighbor_set_fst_subgraph_of_adj {V : Type u} {G : simple_graph V} {v w : V} (hvw : G.adj v w) :
@[simp]
theorem simple_graph.neighbor_set_snd_subgraph_of_adj {V : Type u} {G : simple_graph V} {v w : V} (hvw : G.adj v w) :
@[simp]
theorem simple_graph.neighbor_set_subgraph_of_adj_of_ne_of_ne {V : Type u} {G : simple_graph V} {u v w : V} (hvw : G.adj v w) (hv : u v) (hw : u w) :
theorem simple_graph.neighbor_set_subgraph_of_adj {V : Type u} {G : simple_graph V} [decidable_eq V] {u v w : V} (hvw : G.adj v w) :
(G.subgraph_of_adj hvw).neighbor_set u = ite (u = v) {w} ite (u = w) {v}

Subgraphs of subgraphs #

@[protected, reducible]

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

Equations
@[protected, reducible]

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

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) :
(G'.delete_edges s).adj v w G'.adj v w (v, w) s
@[simp]
theorem simple_graph.subgraph.delete_edges_delete_edges {V : Type u} {G : simple_graph V} {G' : G.subgraph} (s 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') :
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.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'
theorem simple_graph.subgraph.subgraph_of_adj_eq_induce {V : Type u} {G : simple_graph V} {v w : V} (hvw : G.adj v w) :
@[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_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') :