Theorems · Theorem · combinatorics

SimpleGraph.card_interedges_add_card_interedges_compl

∀ {α : Type u_4} (G : SimpleGraph α) [inst : DecidableRel G.Adj] {s t : Finset α} [inst_1 : DecidableEq α],
  Disjoint s t → (G.interedges s t).card + (Gᶜ.interedges s t).card = s.card * t.card

Defined in

Mathlib.Combinatorics.SimpleGraph.Density

Cited by

1 results in Mathlib

Foundations

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

Assumes

DecidableRelDecidableEq