Deletion of edges and vertices

This file defines the deletion of edges and vertices from a graph.

Main definitions

• restrict: the subgraph of G restricted to the edges in F without removing vertices
• deleteEdges: the subgraph of G with the edges in F deleted
• induce: the subgraph of G induced by the set X of vertices
• deleteVerts : the graph obtained from G by deleting the set X of vertices

Tags

graphs, edge deletion, vertex deletion

def Graph.restrict {α : Type u_1} {β : Type u_2} (G : Graph α β) (E₀ : Set β) : Graph α β

Restrict G : Graph α β to the edges in a set E₀ without removing vertices

@[simp]

theorem Graph.edgeSet_restrict {α : Type u_1} {β : Type u_2} (G : Graph α β) (E₀ : Set β) : (G.restrict E₀).edgeSet = G.edgeSet ∩ E₀

@[simp]

theorem Graph.restrict_isLink {α : Type u_1} {β : Type u_2} (G : Graph α β) (E₀ : Set β) (e : β) (x y : α) : (G.restrict E₀).IsLink e x y = (e ∈ E₀ ∧ G.IsLink e x y)

@[simp]

theorem Graph.vertexSet_restrict {α : Type u_1} {β : Type u_2} (G : Graph α β) (E₀ : Set β) : (G.restrict E₀).vertexSet = G.vertexSet

@[simp]

theorem Graph.restrict_le {α : Type u_1} {β : Type u_2} {G : Graph α β} {E₀ : Set β} : G.restrict E₀ ≤ G

@[simp]

theorem Graph.restrict_eq_self_iff {α : Type u_1} {β : Type u_2} (G : Graph α β) (E₀ : Set β) : G.restrict E₀ = G ↔ G.edgeSet ⊆ E₀

@[simp]

theorem Graph.restrict_self {α : Type u_1} {β : Type u_2} (G : Graph α β) : G.restrict G.edgeSet = G

@[simp]

theorem Graph.restrict_edgeSet_inter {α : Type u_1} {β : Type u_2} (G : Graph α β) (F : Set β) : G.restrict (G.edgeSet ∩ F) = G.restrict F

@[simp]

theorem Graph.restrict_inter_edgeSet {α : Type u_1} {β : Type u_2} (G : Graph α β) (F : Set β) : G.restrict (F ∩ G.edgeSet) = G.restrict F

theorem Graph.restrict_mono_left {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : H ≤ G) (F : Set β) : H.restrict F ≤ G.restrict F

theorem Graph.restrict_mono_right {α : Type u_1} {β : Type u_2} {F F₀ : Set β} (G : Graph α β) (hss : F₀ ⊆ F) : G.restrict F₀ ≤ G.restrict F

@[simp]

theorem Graph.restrict_inc {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} {F : Set β} : (G.restrict F).Inc e x ↔ G.Inc e x ∧ e ∈ F

@[simp]

theorem Graph.restrict_isLoopAt {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} {F : Set β} : (G.restrict F).IsLoopAt e x ↔ G.IsLoopAt e x ∧ e ∈ F

@[simp]

theorem Graph.restrict_restrict {α : Type u_1} {β : Type u_2} (G : Graph α β) (F₁ F₂ : Set β) : (G.restrict F₁).restrict F₂ = G.restrict (F₁ ∩ F₂)

def Graph.deleteEdges {α : Type u_1} {β : Type u_2} (G : Graph α β) (F : Set β) : Graph α β

Delete a set F of edges from G. This is a special case of restrict, but we define it with copy so that the edge set is definitionally equal to E(G) \ F.

@[simp]

theorem Graph.edgeSet_deleteEdges {α : Type u_1} {β : Type u_2} (G : Graph α β) (F : Set β) : (G.deleteEdges F).edgeSet = G.edgeSet \ F

@[simp]

theorem Graph.deleteEdges_isLink {α : Type u_1} {β : Type u_2} (G : Graph α β) (F : Set β) (e : β) (x y : α) : (G.deleteEdges F).IsLink e x y = (G.IsLink e x y ∧ e ∉ F)

@[simp]

theorem Graph.vertexSet_deleteEdges {α : Type u_1} {β : Type u_2} (G : Graph α β) (F : Set β) : (G.deleteEdges F).vertexSet = G.vertexSet

@[simp]

theorem Graph.restrict_edgeSet_sdiff_eq_deleteEdges {α : Type u_1} {β : Type u_2} (G : Graph α β) (F : Set β) : G.restrict (G.edgeSet \ F) = G.deleteEdges F

@[deprecated Graph.restrict_edgeSet_sdiff_eq_deleteEdges (since := "2026-06-03")]

theorem Graph.restrict_edgeSet_diff_eq_deleteEdges {α : Type u_1} {β : Type u_2} (G : Graph α β) (F : Set β) : G.restrict (G.edgeSet \ F) = G.deleteEdges F

Alias of Graph.restrict_edgeSet_sdiff_eq_deleteEdges.

@[simp]

theorem Graph.deleteEdges_le {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} : G.deleteEdges F ≤ G

theorem Graph.restrict_eq_deleteEdges {α : Type u_1} {β : Type u_2} (G : Graph α β) (F : Set β) : G.restrict F = G.deleteEdges (G.edgeSet \ F)

@[simp]

theorem Graph.deleteEdges_empty {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.deleteEdges ∅ = G

theorem Graph.deleteEdges_mono_left {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : H ≤ G) (F : Set β) : H.deleteEdges F ≤ G.deleteEdges F

@[simp]

theorem Graph.deleteEdges_inc {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} {F : Set β} : (G.deleteEdges F).Inc e x ↔ G.Inc e x ∧ e ∉ F

@[simp]

theorem Graph.deleteEdges_isLoopAt {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} {F : Set β} : (G.deleteEdges F).IsLoopAt e x ↔ G.IsLoopAt e x ∧ e ∉ F

@[simp]

theorem Graph.deleteEdges_deleteEdges {α : Type u_1} {β : Type u_2} (G : Graph α β) (F₁ F₂ : Set β) : (G.deleteEdges F₁).deleteEdges F₂ = G.deleteEdges (F₁ ∪ F₂)

def Graph.induce {α : Type u_1} {β : Type u_2} (G : Graph α β) (X : Set α) : Graph α β

The subgraph of G induced by a set X of vertices. The edges are the edges of G with both ends in X. (X is not required to be a subset of V(G) for this definition to work, even though this is the standard use case)

@[simp]

theorem Graph.induce_isLink {α : Type u_1} {β : Type u_2} (G : Graph α β) (X : Set α) (e : β) (x y : α) : (G.induce X).IsLink e x y = (G.IsLink e x y ∧ x ∈ X ∧ y ∈ X)

@[simp]

theorem Graph.vertexSet_induce {α : Type u_1} {β : Type u_2} (G : Graph α β) (X : Set α) : (G.induce X).vertexSet = X

theorem Graph.induce_le {α : Type u_1} {β : Type u_2} {G : Graph α β} {X : Set α} (hX : X ⊆ G.vertexSet) : G.induce X ≤ G

@[simp]

theorem Graph.induce_le_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {X : Set α} : G.induce X ≤ G ↔ X ⊆ G.vertexSet

theorem Graph.edgeSet_induce {α : Type u_1} {β : Type u_2} (G : Graph α β) (X : Set α) : (G.induce X).edgeSet = {e : β | ∃ (x : α) (y : α), G.IsLink e x y ∧ x ∈ X ∧ y ∈ X}

@[simp]

theorem Graph.induce_vertexSet {α : Type u_1} {β : Type u_2} (G : Graph α β) : G.induce G.vertexSet = G

def Graph.deleteVerts {α : Type u_1} {β : Type u_2} (G : Graph α β) (X : Set α) : Graph α β

The graph obtained from G by deleting a set of vertices.

@[simp]

theorem Graph.vertexSet_deleteVerts {α : Type u_1} {β : Type u_2} (G : Graph α β) (X : Set α) : (G.deleteVerts X).vertexSet = G.vertexSet \ X

@[simp]

theorem Graph.deleteVerts_isLink {α : Type u_1} {β : Type u_2} {x y : α} {e : β} (G : Graph α β) (X : Set α) : (G.deleteVerts X).IsLink e x y ↔ G.IsLink e x y ∧ x ∉ X ∧ y ∉ X

@[simp]

theorem Graph.edgeSet_deleteVerts {α : Type u_1} {β : Type u_2} (G : Graph α β) (X : Set α) : (G.deleteVerts X).edgeSet = {e : β | ∃ (x : α) (y : α), G.IsLink e x y ∧ x ∉ X ∧ y ∉ X}

@[simp]

theorem Graph.deleteVerts_empty {α : Type u_1} {β : Type u_2} (G : Graph α β) : G.deleteVerts ∅ = G

@[simp]

theorem Graph.deleteVerts_le {α : Type u_1} {β : Type u_2} {G : Graph α β} {X : Set α} : G.deleteVerts X ≤ G