English
Deleting the incidence set x yields an edgeFinset equal to the edgeFinset of G set-differenced by the incidence set of x.
Русский
Удаление инцидентного множества x даёт edgeFinset, равный ребрам G, взятым за разность множеств с IncidenceSet(x).
LaTeX
$$$ (G.deleteIncidenceSet x).edgeFinset = G.edgeFinset \ G.incidenceFinset x $$$
Lean4
/-- The finite edge set of `G.deleteIncidenceSet x` is the finite edge set of the simple graph `G`
set difference the finite incidence set of the vertex `x`. -/
theorem edgeFinset_deleteIncidenceSet_eq_sdiff (G : SimpleGraph V) [DecidableRel G.Adj] (x : V) :
(G.deleteIncidenceSet x).edgeFinset = G.edgeFinset \ G.incidenceFinset x :=
by
rw [incidenceFinset, ← Set.toFinset_diff, Set.toFinset_inj]
exact G.edgeSet_deleteIncidenceSet x