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 #

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
adj_sub : ∀ {v w : V}, self.adj v w → G.adj v w
edge_vert : ∀ {v w : V}, self.adj v w → v ∈ 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

simple_graph.subgraph.has_sizeof_inst
simple_graph.subgraph.lattice
simple_graph.subgraph.bounded_order
simple_graph.subgraph.subgraph_inhabited

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

@[protected]

theorem simple_graph.subgraph.loopless {V : Type u} {G : simple_graph V} (G' : G.subgraph) :

irreflexive G'.adj

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]

def simple_graph.subgraph.coe {V : Type u} {G : simple_graph V} (G' : G.subgraph) :

simple_graph ↥(G'.verts)

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

Equations

G'.coe = {adj := λ (v w : ↥(G'.verts)), G'.adj ↑v ↑w, symm := _, loopless := _}

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

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

G'.is_spanning = ∀ (v : V), v ∈ G'.verts

theorem simple_graph.subgraph.is_spanning_iff {V : Type u} {G : simple_graph V} {G' : G.subgraph} :

G'.is_spanning ↔ G'.verts = set.univ

@[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]

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

G'.spanning_coe = {adj := G'.adj, symm := _, loopless := _}

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

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

↑(⇑(G'.spanning_coe_equiv_coe_of_spanning h) v) = v

def simple_graph.subgraph.spanning_coe_equiv_coe_of_spanning {V : Type u} {G : simple_graph V} (G' : G.subgraph) (h : G'.is_spanning) :

G'.spanning_coe ≃g G'.coe

spanning_coe is equivalent to coe for a subgraph that is_spanning.

Equations

G'.spanning_coe_equiv_coe_of_spanning h = {to_equiv := {to_fun := λ (v : V), ⟨v, _⟩, inv_fun := λ (v : ↥(G'.verts)), ↑v, left_inv := _, right_inv := _}, map_rel_iff' := _}

@[simp]

theorem simple_graph.subgraph.spanning_coe_equiv_coe_of_spanning_symm_apply {V : Type u} {G : simple_graph V} (G' : G.subgraph) (h : G'.is_spanning) (v : ↥(G'.verts)) :

⇑(rel_iso.symm (G'.spanning_coe_equiv_coe_of_spanning h)) v = ↑v

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

G'.is_induced = ∀ {v w : V}, v ∈ G'.verts → w ∈ G'.verts → G.adj v w → G'.adj v w

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

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

Equations

H.support = rel.dom H.adj

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

theorem simple_graph.subgraph.support_subset_verts {V : Type u} {G : simple_graph V} (H : G.subgraph) :

H.support ⊆ H.verts

def simple_graph.subgraph.neighbor_set {V : Type u} {G : simple_graph V} (G' : G.subgraph) (v : V) :

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

Equations

G'.neighbor_set v = set_of (G'.adj v)

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

G'.neighbor_set v ⊆ G.neighbor_set v

theorem simple_graph.subgraph.neighbor_set_subset_verts {V : Type u} {G : simple_graph V} (G' : G.subgraph) (v : V) :

G'.neighbor_set v ⊆ G'.verts

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

def simple_graph.subgraph.coe_neighbor_set_equiv {V : Type u} {G : simple_graph V} {G' : G.subgraph} (v : ↥(G'.verts)) :

↥(G'.coe.neighbor_set v) ≃ ↥(G'.neighbor_set ↑v)

A subgraph as a graph has equivalent neighbor sets.

Equations

simple_graph.subgraph.coe_neighbor_set_equiv v = {to_fun := λ (w : ↥(G'.coe.neighbor_set v)), ⟨↑w, _⟩, inv_fun := λ (w : ↥(G'.neighbor_set ↑v)), ⟨⟨↑w, _⟩, _⟩, left_inv := _, right_inv := _}

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

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

Equations

G'.edge_set = sym2.from_rel _

theorem simple_graph.subgraph.edge_set_subset {V : Type u} {G : simple_graph V} (G' : G.subgraph) :

G'.edge_set ⊆ G.edge_set

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

def simple_graph.subgraph.incidence_set {V : Type u} {G : simple_graph V} (G' : G.subgraph) (v : V) :

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

Equations

G'.incidence_set v = {e ∈ G'.edge_set | v ∈ e}

theorem simple_graph.subgraph.incidence_set_subset_incidence_set {V : Type u} {G : simple_graph V} (G' : G.subgraph) (v : V) :

G'.incidence_set v ⊆ G.incidence_set v

theorem simple_graph.subgraph.incidence_set_subset {V : Type u} {G : simple_graph V} (G' : G.subgraph) (v : V) :

G'.incidence_set v ⊆ G'.edge_set

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

G'.vert v h = ⟨v, h⟩

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

G'.copy V'' hV adj' hadj = {verts := V'', adj := adj', adj_sub := _, edge_vert := _, symm := _}

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

x.union y = {verts := x.verts ∪ y.verts, adj := x.adj ⊔ y.adj, adj_sub := _, edge_vert := _, symm := _}

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

The intersection of two subgraphs.

Equations

x.inter y = {verts := x.verts ∩ y.verts, adj := x.adj ⊓ y.adj, adj_sub := _, edge_vert := _, symm := _}

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

The top subgraph is G as a subgraph of itself.

Equations

simple_graph.subgraph.top = {verts := set.univ V, adj := G.adj, adj_sub := _, edge_vert := _, symm := _}

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

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

Equations

simple_graph.subgraph.bot = {verts := ∅, adj := ⊥, adj_sub := _, edge_vert := _, symm := _}

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

x.is_subgraph y = (x.verts ⊆ y.verts ∧ ∀ ⦃v w : V⦄, x.adj v w → y.adj v w)

@[protected, instance]

def simple_graph.subgraph.lattice {V : Type u} {G : simple_graph V} :

lattice G.subgraph

Equations

simple_graph.subgraph.lattice = {sup := simple_graph.subgraph.union G, le := simple_graph.subgraph.is_subgraph G, lt := semilattice_sup.lt._default simple_graph.subgraph.is_subgraph, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := simple_graph.subgraph.inter G, inf_le_left := _, inf_le_right := _, le_inf := _}

@[protected, instance]

def simple_graph.subgraph.bounded_order {V : Type u} {G : simple_graph V} :

bounded_order G.subgraph

Equations

simple_graph.subgraph.bounded_order = {top := simple_graph.subgraph.top G, le_top := _, bot := simple_graph.subgraph.bot G, bot_le := _}

@[simp]

theorem simple_graph.subgraph.subgraph_inhabited_default {V : Type u} {G : simple_graph V} :

inhabited.default = ⊥

@[protected, instance]

def simple_graph.subgraph.subgraph_inhabited {V : Type u} {G : simple_graph V} :

inhabited G.subgraph

Equations

simple_graph.subgraph.subgraph_inhabited = {default := ⊥}

@[simp]

theorem simple_graph.subgraph.top_verts {V : Type u} {G : simple_graph V} :

⊤.verts = set.univ

@[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]

theorem simple_graph.subgraph.bot_verts {V : Type u} {G : simple_graph V} :

⊥.verts = ∅

@[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.edge_set_top {V : Type u} {G : simple_graph V} :

⊤.edge_set = G.edge_set

@[simp]

theorem simple_graph.subgraph.edge_set_bot {V : Type u} {G : simple_graph V} :

⊥.edge_set = ∅

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

⊤.spanning_coe = G

@[simp]

theorem simple_graph.subgraph.spanning_coe_bot {V : Type u} {G : simple_graph V} :

⊥.spanning_coe = ⊥

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

H.to_subgraph h = {verts := set.univ V, adj := H.adj, adj_sub := h, edge_vert := _, symm := _}

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

(H.to_subgraph h).verts = set.univ

theorem simple_graph.subgraph.support_mono {V : Type u} {G : simple_graph V} {H H' : G.subgraph} (h : H ≤ H') :

H.support ⊆ H'.support

theorem simple_graph.to_subgraph.is_spanning {V : Type u} {G : simple_graph V} (H : simple_graph V) (h : H ≤ G) :

(H.to_subgraph h).is_spanning

theorem simple_graph.subgraph.spanning_coe_le_of_le {V : Type u} {G : simple_graph V} {H H' : G.subgraph} (h : H ≤ H') :

H.spanning_coe ≤ H'.spanning_coe

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

simple_graph.subgraph.top_equiv = {to_equiv := {to_fun := λ (v : ↥(⊤.verts)), ↑v, inv_fun := λ (v : V), ⟨v, trivial⟩, left_inv := _, right_inv := _}, map_rel_iff' := _}

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

⊥.coe ≃g ⊥

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

Equations

simple_graph.subgraph.bot_equiv = {to_equiv := {to_fun := λ (v : ↥(⊥.verts)), false.elim _, inv_fun := λ (v : empty), v.elim, left_inv := _, right_inv := _}, map_rel_iff' := _}

theorem simple_graph.subgraph.edge_set_mono {V : Type u} {G : simple_graph V} {H₁ H₂ : G.subgraph} (h : H₁ ≤ H₂) :

H₁.edge_set ≤ H₂.edge_set

theorem disjoint.edge_set {V : Type u} {G : simple_graph V} {H₁ H₂ : G.subgraph} (h : disjoint H₁ H₂) :

disjoint H₁.edge_set 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) :

(simple_graph.subgraph.map f H).verts = ⇑f '' H.verts

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

simple_graph.subgraph.map f H = {verts := ⇑f '' H.verts, adj := relation.map H.adj ⇑f ⇑f, adj_sub := _, edge_vert := _, symm := _}

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

theorem simple_graph.subgraph.map_monotone {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G →g G') :

monotone (simple_graph.subgraph.map f)

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

(simple_graph.subgraph.comap f H).verts = ⇑f ⁻¹' H.verts

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

simple_graph.subgraph.comap f H = {verts := ⇑f ⁻¹' H.verts, adj := λ (u v : V), G.adj u v ∧ H.adj (⇑f u) (⇑f v), adj_sub := _, edge_vert := _, symm := _}

theorem simple_graph.subgraph.comap_monotone {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G →g G') :

monotone (simple_graph.subgraph.comap f)

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

simple_graph.subgraph.map f H ≤ H' ↔ H ≤ simple_graph.subgraph.comap f H'

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

↑(⇑(simple_graph.subgraph.inclusion h) v) = ↑v

def simple_graph.subgraph.inclusion {V : Type u} {G : simple_graph V} {x 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

simple_graph.subgraph.inclusion h = {to_fun := λ (v : ↥(x.verts)), ⟨↑v, _⟩, map_rel' := _}

theorem simple_graph.subgraph.inclusion.injective {V : Type u} {G : simple_graph V} {x y : G.subgraph} (h : x ≤ y) :

function.injective ⇑(simple_graph.subgraph.inclusion h)

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

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

Equations

x.hom = {to_fun := λ (v : ↥(x.verts)), ↑v, map_rel' := _}

theorem simple_graph.subgraph.hom.injective {V : Type u} {G : simple_graph V} {x : G.subgraph} :

function.injective ⇑(x.hom)

def simple_graph.subgraph.spanning_hom {V : Type u} {G : simple_graph V} (x : G.subgraph) :

x.spanning_coe →g G

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

Equations

x.spanning_hom = {to_fun := id V, map_rel' := _}

@[simp]

theorem simple_graph.subgraph.spanning_hom_apply {V : Type u} {G : simple_graph V} (x : G.subgraph) (a : V) :

⇑(x.spanning_hom) a = id a

theorem simple_graph.subgraph.spanning_hom.injective {V : Type u} {G : simple_graph V} {x : G.subgraph} :

function.injective ⇑(x.spanning_hom)

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

x.neighbor_set v ⊆ y.neighbor_set 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

simple_graph.subgraph.neighbor_set.decidable_pred G' v = h v

@[protected, instance]

def simple_graph.subgraph.finite_at {V : Type u} {G : simple_graph V} {G' : G.subgraph} (v : ↥(G'.verts)) [decidable_rel G'.adj] [fintype ↥(G.neighbor_set ↑v)] :

fintype ↥(G'.neighbor_set ↑v)

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

Equations

simple_graph.subgraph.finite_at v = (G.neighbor_set ↑v).fintype_subset _

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

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

simple_graph.subgraph.finite_at_of_subgraph h v = (G''.neighbor_set ↑v).fintype_subset _

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

fintype ↥(G'.neighbor_set v)

Equations

simple_graph.subgraph.neighbor_set.fintype G' v = G'.verts.fintype_subset _

@[protected, instance]

def simple_graph.subgraph.coe_finite_at {V : Type u} {G : simple_graph V} {G' : G.subgraph} (v : ↥(G'.verts)) [fintype ↥(G'.neighbor_set ↑v)] :

fintype ↥(G'.coe.neighbor_set v)

Equations

simple_graph.subgraph.coe_finite_at v = fintype.of_equiv ↥(G'.neighbor_set ↑v) (simple_graph.subgraph.coe_neighbor_set_equiv v).symm

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

G'.verts.to_finset.card = fintype.card V

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

G'.degree v = fintype.card ↥(G'.neighbor_set v)

theorem simple_graph.subgraph.finset_card_neighbor_set_eq_degree {V : Type u} {G : simple_graph V} {G' : G.subgraph} {v : V} [fintype ↥(G'.neighbor_set v)] :

(G'.neighbor_set v).to_finset.card = G'.degree v

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_spanning_coe {V : Type u} {G : simple_graph V} {G' : G.subgraph} (v : V) [fintype ↥(G'.neighbor_set v)] [fintype ↥(G'.spanning_coe.neighbor_set v)] :

G'.spanning_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

Subgraphs of subgraphs #

@[protected, reducible]

def simple_graph.subgraph.coe_subgraph {V : Type u} {G : simple_graph V} {G' : G.subgraph} :

G'.coe.subgraph → G.subgraph

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

Equations

simple_graph.subgraph.coe_subgraph = simple_graph.subgraph.map G'.hom

@[protected, reducible]

def simple_graph.subgraph.restrict {V : Type u} {G : simple_graph V} {G' : G.subgraph} :

G.subgraph → G'.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

simple_graph.subgraph.restrict = simple_graph.subgraph.comap G'.hom

theorem simple_graph.subgraph.restrict_coe_subgraph {V : Type u} {G : simple_graph V} {G' : G.subgraph} (G'' : G'.coe.subgraph) :

G''.coe_subgraph.restrict = G''

theorem simple_graph.subgraph.coe_subgraph_injective {V : Type u} {G : simple_graph V} (G' : G.subgraph) :

function.injective simple_graph.subgraph.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

G'.delete_edges s = {verts := G'.verts, adj := G'.adj \ sym2.to_rel s, adj_sub := _, edge_vert := _, symm := _}

@[simp]

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

(G'.delete_edges s).verts = G'.verts

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

(G'.delete_edges s).delete_edges s' = G'.delete_edges (s ∪ s')

@[simp]

theorem simple_graph.subgraph.delete_edges_empty_eq {V : Type u} {G : simple_graph V} {G' : G.subgraph} :

G'.delete_edges ∅ = G'

@[simp]

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

G'.spanning_coe.delete_edges s = (G'.delete_edges s).spanning_coe

theorem simple_graph.subgraph.delete_edges_coe_eq {V : Type u} {G : simple_graph V} {G' : G.subgraph} (s : set (sym2 ↥(G'.verts))) :

G'.coe.delete_edges s = (G'.delete_edges (sym2.map coe '' s)).coe

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

(G'.delete_edges s).coe = G'.coe.delete_edges (sym2.map coe ⁻¹' s)

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

G'.delete_edges s ≤ G'

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

G'.delete_edges s' ≤ G'.delete_edges s

@[simp]

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

G'.delete_edges (G'.edge_set ∩ s) = G'.delete_edges s

@[simp]

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

G'.delete_edges (s ∩ G'.edge_set) = G'.delete_edges s

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

(G'.delete_edges s).coe ≤ G'.coe

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

(G'.delete_edges s).spanning_coe ≤ G'.spanning_coe

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

G'.induce s = {verts := s, adj := λ (u v : V), u ∈ s ∧ v ∈ s ∧ G'.adj u v, adj_sub := _, edge_vert := _, symm := _}

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

simple_graph.induce s G = (⊤.induce s).coe

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

G'.induce ∅ = ⊥

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

G'.delete_verts s = G'.induce (G'.verts \ s)

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

(G'.delete_verts s).delete_verts s' = G'.delete_verts (s ∪ s')

@[simp]

theorem simple_graph.subgraph.delete_verts_empty {V : Type u} {G : simple_graph V} {G' : G.subgraph} :

G'.delete_verts ∅ = G'

theorem simple_graph.subgraph.delete_verts_le {V : Type u} {G : simple_graph V} {G' : G.subgraph} {s : set V} :

G'.delete_verts s ≤ G'

theorem simple_graph.subgraph.delete_verts_mono {V : Type u} {G : simple_graph V} {s : set V} {G' G'' : G.subgraph} (h : G' ≤ G'') :

G'.delete_verts s ≤ G''.delete_verts s

theorem simple_graph.subgraph.delete_verts_anti {V : Type u} {G : simple_graph V} {G' : G.subgraph} {s s' : set V} (h : s ⊆ s') :

G'.delete_verts s' ≤ G'.delete_verts 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} :

G'.delete_verts (G'.verts ∩ s) = G'.delete_verts s

@[simp]

theorem simple_graph.subgraph.delete_verts_inter_verts_set_right_eq {V : Type u} {G : simple_graph V} {G' : G.subgraph} {s : set V} :

G'.delete_verts (s ∩ G'.verts) = G'.delete_verts s