English
The edge set after deleting the incidence set of x is the edge set of G with the incidence set of x removed.
Русский
Множество ребер после удаления инцидентного множества x равно ребрам G, исключая инцидентные ребра x.
LaTeX
$$$ (G.deleteIncidenceSet x).edgeSet = G.edgeSet \ G.incidenceSet x $$$
Lean4
/-- The edge set of `G.deleteIncidenceSet x` is the edge set of `G` set difference the incidence
set of the vertex `x`. -/
theorem edgeSet_deleteIncidenceSet (G : SimpleGraph V) (x : V) :
(G.deleteIncidenceSet x).edgeSet = G.edgeSet \ G.incidenceSet x := by
simp_rw [deleteIncidenceSet, deleteEdges, edgeSet_sdiff, edgeSet_fromEdgeSet_incidenceSet]