mathlib3 documentation

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

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

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

G.singleton_subgraph v = {verts := {v}, adj := ⊥, adj_sub := _, edge_vert := _, symm := _}

@[simp]

theorem simple_graph.singleton_subgraph_verts {V : Type u} (G : simple_graph V) (v : V) :

(G.singleton_subgraph v).verts = {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

G.subgraph_of_adj hvw = {verts := {v, w}, adj := λ (a b : V), ⟦(v, w)⟧ = ⟦(a, b)⟧, adj_sub := _, edge_vert := _, symm := _}

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

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]

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]

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

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

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

G₁.spanning_coe = G₂.spanning_coe ↔ G₁.adj = G₂.adj

@[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 ⊆ ⇑simple_graph.edge_set G

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

@[protected, instance]

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

has_sup G.subgraph

The union of two subgraphs.

Equations

simple_graph.subgraph.has_sup = {sup := λ (G₁ G₂ : G.subgraph), {verts := G₁.verts ∪ G₂.verts, adj := G₁.adj ⊔ G₂.adj, adj_sub := _, edge_vert := _, symm := _}}

@[protected, instance]

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

has_inf G.subgraph

The intersection of two subgraphs.

Equations

simple_graph.subgraph.has_inf = {inf := λ (G₁ G₂ : G.subgraph), {verts := G₁.verts ∩ G₂.verts, adj := G₁.adj ⊓ G₂.adj, adj_sub := _, edge_vert := _, symm := _}}

@[protected, instance]

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

has_top G.subgraph

The top subgraph is G as a subgraph of itself.

Equations

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

@[protected, instance]

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

has_bot G.subgraph

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

Equations

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

@[protected, instance]

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

has_Sup G.subgraph

Equations

simple_graph.subgraph.has_Sup = {Sup := λ (s : set G.subgraph), {verts := ⋃ (G' : G.subgraph) (H : G' ∈ s), G'.verts, adj := λ (a b : V), ∃ (G' : G.subgraph) (H : G' ∈ s), G'.adj a b, adj_sub := _, edge_vert := _, symm := _}}

@[protected, instance]

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

has_Inf G.subgraph

Equations

simple_graph.subgraph.has_Inf = {Inf := λ (s : set G.subgraph), {verts := ⋂ (G' : G.subgraph) (H : G' ∈ s), G'.verts, adj := λ (a b : V), (∀ ⦃G' : G.subgraph⦄, G' ∈ s → G'.adj a b) ∧ G.adj a b, adj_sub := _, edge_vert := _, symm := _}}

@[simp]

theorem simple_graph.subgraph.sup_adj {V : Type u} {G : simple_graph V} {G₁ G₂ : G.subgraph} {a b : V} :

(G₁ ⊔ G₂).adj a b ↔ G₁.adj a b ∨ G₂.adj a b

@[simp]

theorem simple_graph.subgraph.inf_adj {V : Type u} {G : simple_graph V} {G₁ G₂ : G.subgraph} {a b : V} :

(G₁ ⊓ G₂).adj a b ↔ G₁.adj a b ∧ G₂.adj a b

@[simp]

theorem simple_graph.subgraph.top_adj {V : Type u} {G : simple_graph V} {a b : V} :

⊤.adj a b ↔ G.adj a b

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

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

⊤.verts = set.univ

@[simp]

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

⊥.verts = ∅

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

(has_Inf.Inf s).adj a b ↔ (∀ (G' : G.subgraph), G' ∈ s → G'.adj a b) ∧ G.adj a b

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

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

distrib_lattice G.subgraph

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

Equations

simple_graph.subgraph.distrib_lattice = {sup := distrib_lattice.sup (show distrib_lattice G.subgraph, from function.injective.distrib_lattice (λ (G' : G.subgraph), (G'.verts, G'.spanning_coe)) simple_graph.subgraph.distrib_lattice._proof_1 simple_graph.subgraph.distrib_lattice._proof_2 simple_graph.subgraph.distrib_lattice._proof_3), le := λ (x y : G.subgraph), x.verts ⊆ y.verts ∧ ∀ ⦃v w : V⦄, x.adj v w → y.adj v w, lt := distrib_lattice.lt (show distrib_lattice G.subgraph, from function.injective.distrib_lattice (λ (G' : G.subgraph), (G'.verts, G'.spanning_coe)) simple_graph.subgraph.distrib_lattice._proof_1 simple_graph.subgraph.distrib_lattice._proof_2 simple_graph.subgraph.distrib_lattice._proof_3), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := distrib_lattice.inf (show distrib_lattice G.subgraph, from function.injective.distrib_lattice (λ (G' : G.subgraph), (G'.verts, G'.spanning_coe)) simple_graph.subgraph.distrib_lattice._proof_1 simple_graph.subgraph.distrib_lattice._proof_2 simple_graph.subgraph.distrib_lattice._proof_3), inf_le_left := _, inf_le_right := _, le_inf := _, le_sup_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 := ⊤, le_top := _, bot := ⊥, bot_le := _}

@[protected, instance]

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

complete_distrib_lattice G.subgraph

Equations

simple_graph.subgraph.complete_distrib_lattice = {sup := has_sup.sup simple_graph.subgraph.has_sup, le := has_le.le (preorder.to_has_le G.subgraph), lt := distrib_lattice.lt simple_graph.subgraph.distrib_lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := has_inf.inf simple_graph.subgraph.has_inf, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := has_Sup.Sup simple_graph.subgraph.has_Sup, le_Sup := _, Sup_le := _, Inf := has_Inf.Inf simple_graph.subgraph.has_Inf, Inf_le := _, le_Inf := _, top := ⊤, bot := ⊥, le_top := _, bot_le := _, inf_Sup_le_supr_inf := _, infi_sup_le_sup_Inf := _}

@[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.neighbor_set_sup {V : Type u} {G : simple_graph V} {H H' : G.subgraph} (v : V) :

(H ⊔ H').neighbor_set v = H.neighbor_set v ∪ H'.neighbor_set v

@[simp]

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

(H ⊓ H').neighbor_set v = H.neighbor_set v ∩ H'.neighbor_set v

@[simp]

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

⊤.neighbor_set v = G.neighbor_set v

@[simp]

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

⊥.neighbor_set v = ∅

@[simp]

theorem simple_graph.subgraph.neighbor_set_Sup {V : Type u} {G : simple_graph V} (s : set G.subgraph) (v : V) :

(has_Sup.Sup s).neighbor_set 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) :

(has_Inf.Inf s).neighbor_set 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]

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

⊤.edge_set = ⇑simple_graph.edge_set G

@[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.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) ∩ ⇑simple_graph.edge_set G

@[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) ∩ ⇑simple_graph.edge_set G

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

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

simple_graph.subgraph.map f (H ⊔ H') = simple_graph.subgraph.map f H ⊔ simple_graph.subgraph.map f 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) :

(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

Properties of `singleton_subgraph` and `subgraph_of_adj` #

@[protected, instance]

def simple_graph.nonempty_singleton_subgraph_verts {V : Type u} {G : simple_graph V} (v : V) :

nonempty ↥((G.singleton_subgraph v).verts)

@[simp]

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

G.singleton_subgraph v ≤ 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} :

simple_graph.subgraph.map f (G.singleton_subgraph v) = G'.singleton_subgraph (⇑f v)

@[simp]

theorem simple_graph.neighbor_set_singleton_subgraph {V : Type u} {G : simple_graph V} (v w : V) :

(G.singleton_subgraph v).neighbor_set w = ∅

@[simp]

theorem simple_graph.edge_set_singleton_subgraph {V : Type u} {G : simple_graph V} (v : V) :

(G.singleton_subgraph v).edge_set = ∅

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

H = G.singleton_subgraph v ↔ 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) :

nonempty ↥((G.subgraph_of_adj hvw).verts)

@[simp]

theorem simple_graph.edge_set_subgraph_of_adj {V : Type u} {G : simple_graph V} {v w : V} (hvw : G.adj v w) :

(G.subgraph_of_adj hvw).edge_set = {⟦(v, w)⟧}

theorem simple_graph.subgraph_of_adj_symm {V : Type u} {G : simple_graph V} {v w : V} (hvw : G.adj v w) :

G.subgraph_of_adj _ = G.subgraph_of_adj hvw

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

simple_graph.subgraph.map f (G.subgraph_of_adj hvw) = G'.subgraph_of_adj _

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

(G.subgraph_of_adj hvw).neighbor_set u ⊆ {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) :

(G.subgraph_of_adj hvw).neighbor_set 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) :

(G.subgraph_of_adj hvw).neighbor_set w = {v}

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

(G.subgraph_of_adj hvw).neighbor_set u = ∅

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

G.singleton_subgraph u ≤ G.subgraph_of_adj h

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

G.singleton_subgraph v ≤ G.subgraph_of_adj h

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'

theorem simple_graph.subgraph.singleton_subgraph_eq_induce {V : Type u} {G : simple_graph V} {v : V} :

G.singleton_subgraph v = ⊤.induce {v}

theorem simple_graph.subgraph.subgraph_of_adj_eq_induce {V : Type u} {G : simple_graph V} {v w : V} (hvw : G.adj v w) :

G.subgraph_of_adj hvw = ⊤.induce {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

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