# mathlib3documentation

combinatorics.simple_graph.subgraph

# Subgraphs of a simple graph #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

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) :
@[simp]
theorem simple_graph.singleton_subgraph_adj {V : Type u} (G : simple_graph V) (v ᾰ ᾰ_1 : V) :
@[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) :
@[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) :
@[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]
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) :
@[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)) :
@[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) :
@[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) :
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]

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_inj {V : Type u} {G : simple_graph V} {G₁ G₂ : G.subgraph} :
@[simp]

`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) :
@[protected, instance]

The union of two subgraphs.

Equations
@[protected, instance]

The intersection of two subgraphs.

Equations
@[protected, instance]

The `top` subgraph is `G` as a subgraph of itself.

Equations
@[protected, instance]

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

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem simple_graph.subgraph.sup_adj {V : Type u} {G : simple_graph V} {G₁ G₂ : G.subgraph} {a b : V} :
@[simp]
theorem simple_graph.subgraph.inf_adj {V : Type u} {G : simple_graph V} {G₁ G₂ : G.subgraph} {a b : V} :
@[simp]
theorem simple_graph.subgraph.top_adj {V : Type u} {G : simple_graph V} {a b : V} :
@[simp]
theorem simple_graph.subgraph.not_bot_adj {V : Type u} {G : simple_graph V} {a b : V} :
@[simp]
theorem simple_graph.subgraph.verts_sup {V : Type u} {G : simple_graph V} (G₁ G₂ : G.subgraph) :
(G₁ G₂).verts = G₁.verts G₂.verts
@[simp]
theorem simple_graph.subgraph.verts_inf {V : Type u} {G : simple_graph V} (G₁ G₂ : G.subgraph) :
(G₁ G₂).verts = G₁.verts G₂.verts
@[simp]
@[simp]
@[simp]
theorem simple_graph.subgraph.Sup_adj {V : Type u} {G : simple_graph V} {a b : V} {s : set G.subgraph} :
(has_Sup.Sup s).adj a b (G_1 : G.subgraph) (H : G_1 s), G_1.adj a b
@[simp]
theorem simple_graph.subgraph.Inf_adj {V : Type u} {G : simple_graph V} {a b : V} {s : set G.subgraph} :
@[simp]
theorem simple_graph.subgraph.supr_adj {ι : Sort u_1} {V : Type u} {G : simple_graph V} {a b : V} {f : ι G.subgraph} :
( (i : ι), f i).adj a b (i : ι), (f i).adj a b
@[simp]
theorem simple_graph.subgraph.infi_adj {ι : Sort u_1} {V : Type u} {G : simple_graph V} {a b : V} {f : ι G.subgraph} :
( (i : ι), f i).adj a b ( (i : ι), (f i).adj a b) G.adj a b
theorem simple_graph.subgraph.Inf_adj_of_nonempty {V : Type u} {G : simple_graph V} {a b : V} {s : set G.subgraph} (hs : s.nonempty) :
(has_Inf.Inf s).adj a b (G' : G.subgraph), G' s G'.adj a b
theorem simple_graph.subgraph.infi_adj_of_nonempty {ι : Sort u_1} {V : Type u} {G : simple_graph V} {a b : V} [nonempty ι] {f : ι G.subgraph} :
( (i : ι), f i).adj a b (i : ι), (f i).adj a b
@[simp]
theorem simple_graph.subgraph.verts_Sup {V : Type u} {G : simple_graph V} (s : set G.subgraph) :
(has_Sup.Sup s).verts = (G' : G.subgraph) (H : G' s), G'.verts
@[simp]
theorem simple_graph.subgraph.verts_Inf {V : Type u} {G : simple_graph V} (s : set G.subgraph) :
(has_Inf.Inf s).verts = (G' : G.subgraph) (H : G' s), G'.verts
@[simp]
theorem simple_graph.subgraph.verts_supr {ι : Sort u_1} {V : Type u} {G : simple_graph V} {f : ι G.subgraph} :
( (i : ι), f i).verts = (i : ι), (f i).verts
@[simp]
theorem simple_graph.subgraph.verts_infi {ι : Sort u_1} {V : Type u} {G : simple_graph V} {f : ι G.subgraph} :
( (i : ι), f i).verts = (i : ι), (f i).verts
@[protected, instance]

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

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem simple_graph.subgraph.neighbor_set_sup {V : Type u} {G : simple_graph V} {H H' : G.subgraph} (v : V) :
@[simp]
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.neighbor_set_top {V : Type u} {G : simple_graph V} (v : V) :
@[simp]
theorem simple_graph.subgraph.neighbor_set_bot {V : Type u} {G : simple_graph V} (v : V) :
@[simp]
theorem simple_graph.subgraph.neighbor_set_Sup {V : Type u} {G : simple_graph V} (s : set G.subgraph) (v : V) :
v = (G' : G.subgraph) (H : G' s), G'.neighbor_set v
@[simp]
theorem simple_graph.subgraph.neighbor_set_Inf {V : Type u} {G : simple_graph V} (s : set G.subgraph) (v : V) :
v = ( (G' : G.subgraph) (H : G' s), G'.neighbor_set v) G.neighbor_set v
@[simp]
theorem simple_graph.subgraph.neighbor_set_supr {ι : Sort u_1} {V : Type u} {G : simple_graph V} (f : ι G.subgraph) (v : V) :
( (i : ι), f i).neighbor_set v = (i : ι), (f i).neighbor_set v
@[simp]
theorem simple_graph.subgraph.neighbor_set_infi {ι : Sort u_1} {V : Type u} {G : simple_graph V} (f : ι G.subgraph) (v : V) :
( (i : ι), f i).neighbor_set v = ( (i : ι), (f i).neighbor_set v) G.neighbor_set v
@[simp]
@[simp]
@[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.edge_set_Sup {V : Type u} {G : simple_graph V} (s : set G.subgraph) :
(has_Sup.Sup s).edge_set = (G' : G.subgraph) (H : G' s), G'.edge_set
@[simp]
theorem simple_graph.subgraph.edge_set_Inf {V : Type u} {G : simple_graph V} (s : set G.subgraph) :
(has_Inf.Inf s).edge_set = ( (G' : G.subgraph) (H : G' s), G'.edge_set)
@[simp]
theorem simple_graph.subgraph.edge_set_supr {ι : Sort u_1} {V : Type u} {G : simple_graph V} (f : ι G.subgraph) :
( (i : ι), f i).edge_set = (i : ι), (f i).edge_set
@[simp]
theorem simple_graph.subgraph.edge_set_infi {ι : Sort u_1} {V : Type u} {G : simple_graph V} (f : ι G.subgraph) :
( (i : ι), f i).edge_set = ( (i : ι), (f i).edge_set)
@[simp]
@[simp]
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.subgraph.spanning_coe_le_of_le {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₂) :
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') :
theorem simple_graph.subgraph.map_sup {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G →g G') {H H' : G.subgraph} :
(H H') =
@[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

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
@[protected, 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. 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) :
H v H.verts
@[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} :
@[simp]
theorem simple_graph.neighbor_set_singleton_subgraph {V : Type u} {G : simple_graph V} (v w : V) :
w =
theorem simple_graph.eq_singleton_subgraph_iff_verts_eq {V : Type u} {G : simple_graph V} (H : G.subgraph) {v : V} :
H = H.verts = {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}
theorem simple_graph.singleton_subgraph_fst_le_subgraph_of_adj {V : Type u} {G : simple_graph V} {u v : V} {h : G.adj u v} :
theorem simple_graph.singleton_subgraph_snd_le_subgraph_of_adj {V : Type u} {G : simple_graph V} {u v : V} {h : G.adj u 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) :
@[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_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_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') :