Edge deletion

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

Main definitions

• SimpleGraph.deleteEdges G s is the simple graph G with the edges s : Set (Sym2 V) removed from the edge set.

• SimpleGraph.deleteIncidenceSet G v is the simple graph G with the incidence set of v removed from the edge set.

• SimpleGraph.deleteFar G p r is the predicate that a graph is r-delete-far from a property p, that is, at least r edges must be deleted to satisfy p.

def SimpleGraph.deleteEdges {V : Type u_1} (G : SimpleGraph V) (s : Set (Sym2 V)) : SimpleGraph 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.

instance SimpleGraph.instDecidableRelAdjDeleteEdgesOfDecidablePredSym2MemSetOfDecidableEq {V : Type u_1} {G : SimpleGraph V} {s : Set (Sym2 V)} [DecidableRel G.Adj] [DecidablePred fun (x : Sym2 V) => x ∈ s] [DecidableEq V] : DecidableRel (G.deleteEdges s).Adj

@[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) : G.deleteEdges G'.edgeSet = G \ G'

@[simp]

theorem SimpleGraph.deleteEdges_deleteEdges {V : Type u_1} {G : SimpleGraph V} (s s' : Set (Sym2 V)) : (G.deleteEdges s).deleteEdges s' = G.deleteEdges (s ∪ s')

theorem SimpleGraph.deleteEdges_empty {V : Type u_1} {G : SimpleGraph V} : G.deleteEdges ∅ = G

@[simp]

theorem SimpleGraph.deleteEdges_univ {V : Type u_1} {G : SimpleGraph V} : G.deleteEdges Set.univ = ⊥

theorem SimpleGraph.deleteEdges_le {V : Type u_1} {G : SimpleGraph V} (s : Set (Sym2 V)) : G.deleteEdges s ≤ G

theorem SimpleGraph.deleteEdges_anti {V : Type u_1} {G : SimpleGraph V} {s₁ s₂ : Set (Sym2 V)} (h : s₁ ⊆ s₂) : G.deleteEdges s₂ ≤ G.deleteEdges s₁

theorem SimpleGraph.deleteEdges_mono {V : Type u_1} {G H : SimpleGraph V} {s : Set (Sym2 V)} (h : G ≤ H) : G.deleteEdges s ≤ H.deleteEdges s

@[simp]

theorem SimpleGraph.deleteEdges_eq_self {V : Type u_1} {G : SimpleGraph V} {s : Set (Sym2 V)} : G.deleteEdges s = G ↔ Disjoint G.edgeSet s

theorem SimpleGraph.deleteEdges_eq_inter_edgeSet {V : Type u_1} {G : SimpleGraph V} (s : Set (Sym2 V)) : G.deleteEdges s = G.deleteEdges (s ∩ G.edgeSet)

@[simp]

theorem SimpleGraph.deleteEdges_of_subset_diagSet {V : Type u_1} {s : Set (Sym2 V)} (G : SimpleGraph V) (hs : s ⊆ Sym2.diagSet) : G.deleteEdges s = G

theorem SimpleGraph.deleteEdges_sdiff_eq_of_le {V : Type u_1} {G H : SimpleGraph V} (h : H ≤ G) : G.deleteEdges (G.edgeSet \ H.edgeSet) = H

@[simp]

theorem SimpleGraph.edgeSet_deleteEdges {V : Type u_1} {G : SimpleGraph V} (s : Set (Sym2 V)) : (G.deleteEdges s).edgeSet = G.edgeSet \ s

@[simp]

theorem SimpleGraph.edgeFinset_deleteEdges {V : Type u_1} {G : SimpleGraph V} [DecidableEq V] [Fintype ↑G.edgeSet] (s : Finset (Sym2 V)) [Fintype ↑(G.deleteEdges ↑s).edgeSet] : (G.deleteEdges ↑s).edgeFinset = G.edgeFinset \ s

@[simp]

theorem SimpleGraph.deleteEdges_sup {V : Type u_1} (G H : SimpleGraph V) (s : Set (Sym2 V)) : (G ⊔ H).deleteEdges s = G.deleteEdges s ⊔ H.deleteEdges s

@[simp]

theorem SimpleGraph.deleteEdges_fromEdgeSet {V : Type u_1} (s t : Set (Sym2 V)) : (fromEdgeSet s).deleteEdges t = fromEdgeSet (s \ t)

def SimpleGraph.deleteIncidenceSet {V : Type u_1} (G : SimpleGraph V) (x : V) : SimpleGraph V

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

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

theorem SimpleGraph.deleteIncidenceSet_le {V : Type u_1} (G : SimpleGraph V) (x : V) : G.deleteIncidenceSet x ≤ G

theorem SimpleGraph.edgeSet_fromEdgeSet_incidenceSet {V : Type u_1} (G : SimpleGraph V) (x : V) : (fromEdgeSet (G.incidenceSet x)).edgeSet = G.incidenceSet x

theorem SimpleGraph.edgeSet_deleteIncidenceSet {V : Type u_1} (G : SimpleGraph V) (x : V) : (G.deleteIncidenceSet x).edgeSet = G.edgeSet \ G.incidenceSet x

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

theorem SimpleGraph.support_deleteIncidenceSet_subset {V : Type u_1} (G : SimpleGraph V) (x : V) : (G.deleteIncidenceSet x).support ⊆ G.support \ {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 : x ∉ s) : induce s (G.deleteIncidenceSet x) = induce s G

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.

instance SimpleGraph.instDecidableRelAdjDeleteIncidenceSet {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {x : V} : DecidableRel (G.deleteIncidenceSet x).Adj

theorem SimpleGraph.card_edgeFinset_induce_compl_singleton {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (x : V) : (induce {x}ᶜ G).edgeFinset.card = (G.deleteIncidenceSet x).edgeFinset.card

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

theorem SimpleGraph.edgeFinset_deleteIncidenceSet_eq_sdiff {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (x : V) : (G.deleteIncidenceSet x).edgeFinset = G.edgeFinset \ G.incidenceFinset 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.

theorem SimpleGraph.card_edgeFinset_deleteIncidenceSet {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (x : V) : (G.deleteIncidenceSet x).edgeFinset.card = G.edgeFinset.card - G.degree x

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

theorem SimpleGraph.edgeFinset_deleteIncidenceSet_eq_filter {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (x : V) : (G.deleteIncidenceSet x).edgeFinset = {x_1 ∈ G.edgeFinset | x ∉ x_1}

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

theorem SimpleGraph.card_support_deleteIncidenceSet {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {x : V} (hx : x ∈ G.support) : Fintype.card ↑(G.deleteIncidenceSet x).support ≤ Fintype.card ↑G.support - 1

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 V → Prop) (r : 𝕜) : Prop

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.

theorem SimpleGraph.deleteFar_iff {V : Type u_1} {G : SimpleGraph V} {𝕜 : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [Fintype ↑G.edgeSet] {p : SimpleGraph V → Prop} {r : 𝕜} [Fintype (Sym2 V)] : G.DeleteFar p r ↔ ∀ ⦃H : SimpleGraph V⦄ [inst : DecidableRel H.Adj], H ≤ G → p H → r ≤ ↑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 V → Prop} {r : 𝕜} [Fintype (Sym2 V)] : G.DeleteFar p r → ∀ ⦃H : SimpleGraph V⦄ [inst : DecidableRel H.Adj], H ≤ G → p H → r ≤ ↑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 V → Prop} {r₁ r₂ : 𝕜} (h : G.DeleteFar p r₂) (hr : r₁ ≤ r₂) : G.DeleteFar p r₁

theorem SimpleGraph.DeleteFar.le_card_edgeFinset {V : Type u_1} {G : SimpleGraph V} {𝕜 : Type u_2} [Ring 𝕜] [PartialOrder 𝕜] [Fintype ↑G.edgeSet] {p : SimpleGraph V → Prop} {r : 𝕜} (h : G.DeleteFar p r) (hp : p ⊥) : r ≤ ↑G.edgeFinset.card