Theorems · Theorem · combinatorics

SimpleGraph.card_edgeFinset_replaceVertex_of_adj

∀ {V : Type u_1} (G : SimpleGraph V) {s t : V} [inst : DecidableEq V] [inst_1 : Fintype V]
  [inst_2 : DecidableRel G.Adj],
  G.Adj s t → (G.replaceVertex s t).edgeFinset.card = G.edgeFinset.card + G.degree s - G.degree t - 1

Defined in

Mathlib.Combinatorics.SimpleGraph.Operations

Cited by

1 results in Mathlib

Foundations

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

Assumes

DecidableEqFintypeDecidableRel