Theorems · Theorem · combinatorics

SimpleGraph.IsNClique.of_induce

∀ {α : Type u_1} {G : SimpleGraph α} {S : G.Subgraph} {F : Set α} {s : Finset { x // x ∈ F }} {n : ℕ},
  (S.induce F).coe.IsNClique n s → G.IsNClique n (Finset.map { toFun := Subtype.val, inj' := ⋯ } s)

If a set of vertices A is an n-clique in subgraph of G induced by a superset of A, its embedding is an n-clique in G.

Defined in

Mathlib.Combinatorics.SimpleGraph.Clique

Cited by

0 results in Mathlib

Foundations

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