card_edgeFinset_deleteIncidenceSet

English

Deleting the incidence set of x reduces the edgeFinset by exactly deg(x).

Русский

Удаление инцидентного множества x уменьшает множество ребер на ровно deg(x).

LaTeX

$$$ \#(G.deleteIncidenceSet x).edgeFinset = \#G.edgeFinset - \mathrm{deg}(x) $$$

Lean4

/-- Deleting the incident set of the vertex `x` deletes exactly `G.degree x` edges from the edge
set of the simple graph `G`. -/
theorem card_edgeFinset_deleteIncidenceSet (G : SimpleGraph V) [DecidableRel G.Adj] (x : V) :
    #(G.deleteIncidenceSet x).edgeFinset = #G.edgeFinset - G.degree x := by
  simp_rw [← card_incidenceFinset_eq_degree, ← card_sdiff_of_subset (G.incidenceFinset_subset x),
    edgeFinset_deleteIncidenceSet_eq_sdiff]

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