Theorems · Theorem · combinatorics

SimpleGraph.card_edgeFinset_sup_edge

∀ {V : Type u_1} (G : SimpleGraph V) {s t : V} [inst : Fintype V] [inst_1 : DecidableRel G.Adj]
  [inst_2 : Fintype ↑(G ⊔ SimpleGraph.edge s t).edgeSet],
  ¬G.Adj s t → s ≠ t → (G ⊔ SimpleGraph.edge s t).edgeFinset.card = G.edgeFinset.card + 1

Defined in

Mathlib.Combinatorics.SimpleGraph.Operations

Cited by

1 results in Mathlib

Foundations

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

Assumes

FintypeDecidableRelFintype