edgeFinset_deleteIncidenceSet_eq_filter

English

The edgeFinset after deletion equals the SDiff of the original edgeFinset and the incidenceFinset.

Русский

После удаления инцидентного множества ребра образуют SDiff от исходного edgeFinset и incidenceFinset.

LaTeX

$$$ (G.deleteIncidenceSet x).edgeFinset = \mathrm{Finset}.instSDiff.sdiff G.edgeFinset (G.incidenceFinset x) $$$

Lean4

/-- Deleting the incident set of the vertex `x` is equivalent to filtering the edges of the simple
graph `G` that do not contain `x`. -/
theorem edgeFinset_deleteIncidenceSet_eq_filter (G : SimpleGraph V) [DecidableRel G.Adj] (x : V) :
    (G.deleteIncidenceSet x).edgeFinset = G.edgeFinset.filter (x ∉ ·) :=
  by
  rw [edgeFinset_deleteIncidenceSet_eq_sdiff, sdiff_eq_filter]
  apply filter_congr
  intro _ h
  rw [incidenceFinset, Set.mem_toFinset, incidenceSet, Set.mem_setOf_eq, not_and, Classical.imp_iff_right_iff]
  left
  rwa [mem_edgeFinset] at h

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