Commit 2026-04-15 14:52 c2c71a08

feat(Combinatorics/Graph): graph deletion operations (#35879) This PR adds definitions and basic lemmas for deleting edges and vertices from a graph in Mathlib/Combinatorics/Graph/Delete.lean. It introduces the following operations:

• 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 These definitions are accompanied by simp lemmas describing their edge sets, incidence relations, and basic properties such as monotonicity.