Documentation

Mathlib.Combinatorics.SimpleGraph.DeleteEdges

Edge deletion #

This file defines operations deleting the edges of a simple graph and proves theorems in the finite case.

Main definitions #

def SimpleGraph.deleteEdges {V : Type u_1} (G : SimpleGraph V) (s : Set (Sym2 V)) :

Given a set of vertex pairs, remove all of the corresponding edges from the graph's edge set, if present.

See also: SimpleGraph.Subgraph.deleteEdges.

Equations
@[simp]
theorem SimpleGraph.deleteEdges_adj {V : Type u_1} {v w : V} {G : SimpleGraph V} {s : Set (Sym2 V)} :
(G.deleteEdges s).Adj v w G.Adj v w s(v, w)s
@[simp]
theorem SimpleGraph.deleteEdges_edgeSet {V : Type u_1} (G G' : SimpleGraph V) :
@[simp]
theorem SimpleGraph.deleteEdges_deleteEdges {V : Type u_1} {G : SimpleGraph V} (s s' : Set (Sym2 V)) :
@[simp]
theorem SimpleGraph.deleteEdges_le {V : Type u_1} {G : SimpleGraph V} (s : Set (Sym2 V)) :
theorem SimpleGraph.deleteEdges_anti {V : Type u_1} {G : SimpleGraph V} {s₁ s₂ : Set (Sym2 V)} (h : s₁ s₂) :
theorem SimpleGraph.deleteEdges_mono {V : Type u_1} {G H : SimpleGraph V} {s : Set (Sym2 V)} (h : G H) :
@[simp]
theorem SimpleGraph.deleteEdges_eq_self {V : Type u_1} {G : SimpleGraph V} {s : Set (Sym2 V)} :

Given a vertex x, remove the edges incident to x from the edge set.

Equations
theorem SimpleGraph.deleteIncidenceSet_adj {V : Type u_1} {G : SimpleGraph V} {x v₁ v₂ : V} :
(G.deleteIncidenceSet x).Adj v₁ v₂ G.Adj v₁ v₂ v₁ x v₂ x

The edge set of G.deleteIncidenceSet x is the edge set of G set difference the incidence set of the vertex x.

The support of G.deleteIncidenceSet x is a subset of the support of G set difference the singleton set {x}.

theorem SimpleGraph.induce_deleteIncidenceSet_of_notMem {V : Type u_1} (G : SimpleGraph V) {s : Set V} {x : V} (h : xs) :

If the vertex x is not in the set s, then the induced subgraph in G.deleteIncidenceSet x by s is equal to the induced subgraph in G by s.

@[deprecated SimpleGraph.induce_deleteIncidenceSet_of_notMem (since := "2025-05-23")]
theorem SimpleGraph.induce_deleteIncidenceSet_of_not_mem {V : Type u_1} (G : SimpleGraph V) {s : Set V} {x : V} (h : xs) :

Alias of SimpleGraph.induce_deleteIncidenceSet_of_notMem.


If the vertex x is not in the set s, then the induced subgraph in G.deleteIncidenceSet x by s is equal to the induced subgraph in G by s.

Deleting the incidence set of the vertex x retains the same number of edges as in the induced subgraph of the vertices {x}ᶜ.

The finite edge set of G.deleteIncidenceSet x is the finite edge set of the simple graph G set difference the finite incidence set of the vertex x.

Deleting the incident set of the vertex x deletes exactly G.degree x edges from the edge set of the simple graph G.

Deleting the incident set of the vertex x is equivalent to filtering the edges of the simple graph G that do not contain x.

The support of G.deleteIncidenceSet x is at most 1 less than the support of the simple graph G.

def SimpleGraph.DeleteFar {V : Type u_1} (G : SimpleGraph V) {𝕜 : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [Fintype G.edgeSet] (p : SimpleGraph VProp) (r : 𝕜) :

A graph is r-delete-far from a property p if we must delete at least r edges from it to get a graph with the property p.

Equations
theorem SimpleGraph.deleteFar_iff {V : Type u_1} {G : SimpleGraph V} {𝕜 : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [Fintype G.edgeSet] {p : SimpleGraph VProp} {r : 𝕜} [Fintype (Sym2 V)] :
G.DeleteFar p r ∀ ⦃H : SimpleGraph V⦄ [inst : DecidableRel H.Adj], H Gp Hr G.edgeFinset.card - H.edgeFinset.card
theorem SimpleGraph.DeleteFar.le_card_sub_card {V : Type u_1} {G : SimpleGraph V} {𝕜 : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [Fintype G.edgeSet] {p : SimpleGraph VProp} {r : 𝕜} [Fintype (Sym2 V)] :
G.DeleteFar p r∀ ⦃H : SimpleGraph V⦄ [inst : DecidableRel H.Adj], H Gp Hr G.edgeFinset.card - H.edgeFinset.card

Alias of the forward direction of SimpleGraph.deleteFar_iff.

theorem SimpleGraph.DeleteFar.mono {V : Type u_1} {G : SimpleGraph V} {𝕜 : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [Fintype G.edgeSet] {p : SimpleGraph VProp} {r₁ r₂ : 𝕜} (h : G.DeleteFar p r₂) (hr : r₁ r₂) :
G.DeleteFar p r₁