Theorems · Theorem · combinatorics

SimpleGraph.IsNClique.insert_erase

∀ {α : Type u_1} {G : SimpleGraph α} {n : ℕ} {s : Finset α} {a b : α} [inst : DecidableEq α],
  G.IsNClique n s → (∀ w ∈ s \ {b}, G.Adj a w) → b ∈ s → G.IsNClique n (insert a (s.erase b))

Defined in

Mathlib.Combinatorics.SimpleGraph.Clique

Cited by

0 results in Mathlib

Foundations

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

Assumes

DecidableEq