English
Given a subgraph G' of G and a set s of unordered vertex pairs, form a subgraph by removing from the edge set all edges corresponding to pairs in s.
Русский
Дано подграф G' графа G и множество s неупорядоченных пар вершин; образуется подграф, в котором удаляются все ребра, соответствующие парам из s.
LaTeX
$$$ (G'.deleteEdges(s)).verts = G'.verts \\land (G'.deleteEdges(s)).Adj = G'.Adj \\setminus \\mathrm{ToRel}(s) $$$
Lean4
/-- Given a subgraph `G'` and a set of vertex pairs, remove all of the corresponding edges
from its edge set, if present.
See also: `SimpleGraph.deleteEdges`. -/
def deleteEdges (G' : G.Subgraph) (s : Set (Sym2 V)) : G.Subgraph
where
verts := G'.verts
Adj := G'.Adj \ Sym2.ToRel s
adj_sub h' := G'.adj_sub h'.1
edge_vert h' := G'.edge_vert h'.1
symm a b := by simp [G'.adj_comm, Sym2.eq_swap]
