edgeSet_deleteIncidenceSet — Mathlib

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]

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