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.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.

Equations

• G.deleteEdges s = G \ SimpleGraph.fromEdgeSet s

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

@[simp]

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)

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

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

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

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.

Equations

• G.DeleteFar p r = ∀ ⦃s : Finset (Sym2 V)⦄, s ⊆ G.edgeFinset → p (G.deleteEdges ↑s) → r ≤ ↑s.card

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₁