Theorems · Theorem · combinatorics

SimpleGraph.edgeFinset_deleteIncidenceSet_eq_sdiff

∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj] (x : V),
  (G.deleteIncidenceSet x).edgeFinset = G.edgeFinset \ G.incidenceFinset x

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.

Defined in

Mathlib.Combinatorics.SimpleGraph.DeleteEdges

Cited by

2 results in Mathlib

Foundations

Depth 73 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FintypeDecidableEqDecidableRel