edgeFinset_deleteIncidenceSet_eq_sdiff

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

Похожие утверждения