Deletion in standard multigraphs

This file computes edge deletion Graph.deleteEdges in two families of multigraphs: graphs Graph.ofSimpleGraph H built from simple graphs, where deletion corresponds to SimpleGraph.deleteEdges, and the graphs Graph.banana u w F on two vertices, where deletion removes edges from F. These identities let deletion-based connectivity predicates be compared with their simple-graph versions and evaluated on explicit examples. It also records that deletion is antitone in the deleted set, Graph.deleteEdges_anti_right, complementing Mathlib's Graph.deleteEdges_mono_left, and that it gives a spanning subgraph, Graph.deleteEdges_isSpanningSubgraph. Vertex deletion commutes with simplification up to the canonical isomorphism Graph.toSimpleGraphDeleteVertsIso; its vertex map retains the original point.

theorem Graph.deleteEdges_anti_right {α : Type u_1} {β : Type u_2} (G : Graph α β) {F₁ F₂ : Set β} (h : F₁ ⊆ F₂) : G.deleteEdges F₂ ≤ G.deleteEdges F₁

Deleting more edges gives a smaller graph.

theorem Graph.deleteEdges_isSpanningSubgraph {α : Type u_1} {β : Type u_2} (G : Graph α β) (F : Set β) : G.deleteEdges F ≤s G

Deleting edges keeps every vertex, so it gives a spanning subgraph.

@[simp]

theorem Graph.ofSimpleGraph_deleteEdges {α : Type u_1} (H : SimpleGraph α) (F : Set (Sym2 α)) : (ofSimpleGraph H).deleteEdges F = ofSimpleGraph (H.deleteEdges F)

Deleting edges commutes with regarding a simple graph as a multigraph.

@[simp]

theorem Graph.banana_deleteEdges {α : Type u_1} {β : Type u_2} (u w : α) (F D : Set β) : (banana u w F).deleteEdges D = banana u w (F \ D)

Deleting edges from a graph on two vertices removes them from its edge set.

def Graph.toSimpleGraphDeleteVertsIso {α : Type u_1} {β : Type u_2} (G : Graph α β) (X : Set α) : (G.deleteVerts X).toSimpleGraph ≃g SimpleGraph.induce {v : ↑G.vertexSet | ↑v ∉ X} G.toSimpleGraph

Simplifying after vertex deletion is the same as inducing the simplification on the remaining actual vertices.

@[simp]

theorem Graph.coe_toSimpleGraphDeleteVertsIso_apply {α : Type u_1} {β : Type u_2} (G : Graph α β) (X : Set α) (v : ↑(G.deleteVerts X).vertexSet) : ↑↑((G.toSimpleGraphDeleteVertsIso X) v) = ↑v

@[simp]

theorem Graph.coe_toSimpleGraphDeleteVertsIso_symm_apply {α : Type u_1} {β : Type u_2} (G : Graph α β) (X : Set α) (v : { v : ↑G.vertexSet // ↑v ∉ X }) : ↑((G.toSimpleGraphDeleteVertsIso X).symm v) = ↑↑v