# Documentation

Mathlib.Combinatorics.SimpleGraph.Clique

# Graph cliques #

This file defines cliques in simple graphs. A clique is a set of vertices that are pairwise adjacent.

## Main declarations #

• SimpleGraph.IsClique: Predicate for a set of vertices to be a clique.
• SimpleGraph.IsNClique: Predicate for a set of vertices to be an n-clique.
• SimpleGraph.cliqueFinset: Finset of n-cliques of a graph.
• SimpleGraph.CliqueFree: Predicate for a graph to have no n-cliques.

## TODO #

• Clique numbers
• Do we need cliqueSet, a version of cliqueFinset for infinite graphs?

### Cliques #

@[inline, reducible]
abbrev SimpleGraph.IsClique {α : Type u_1} (G : ) (s : Set α) :

A clique in a graph is a set of vertices that are pairwise adjacent.

Instances For
theorem SimpleGraph.isClique_iff {α : Type u_1} (G : ) {s : Set α} :
theorem SimpleGraph.isClique_iff_induce_eq {α : Type u_1} (G : ) {s : Set α} :

A clique is a set of vertices whose induced graph is complete.

instance SimpleGraph.instDecidableIsCliqueToSet {α : Type u_1} (G : ) [] [DecidableRel G.Adj] {s : } :
theorem SimpleGraph.IsClique.mono {α : Type u_1} {G : } {H : } {s : Set α} (h : G H) :
theorem SimpleGraph.IsClique.subset {α : Type u_1} {G : } {s : Set α} {t : Set α} (h : t s) :
@[simp]
theorem SimpleGraph.isClique_bot_iff {α : Type u_1} {s : Set α} :
theorem SimpleGraph.IsClique.subsingleton {α : Type u_1} {s : Set α} :

Alias of the forward direction of SimpleGraph.isClique_bot_iff.

### n-cliques #

structure SimpleGraph.IsNClique {α : Type u_1} (G : ) (n : ) (s : ) :
• clique :
• card_eq : = n

An n-clique in a graph is a set of n vertices which are pairwise connected.

Instances For
theorem SimpleGraph.isNClique_iff {α : Type u_1} (G : ) {n : } {s : } :
= n
instance SimpleGraph.instDecidableIsNClique {α : Type u_1} (G : ) [] [DecidableRel G.Adj] {n : } {s : } :
theorem SimpleGraph.IsNClique.mono {α : Type u_1} {G : } {H : } {n : } {s : } (h : G H) :
@[simp]
theorem SimpleGraph.isNClique_bot_iff {α : Type u_1} {n : } {s : } :
n 1 = n
theorem SimpleGraph.is3Clique_triple_iff {α : Type u_1} {G : } [] {a : α} {b : α} {c : α} :
theorem SimpleGraph.is3Clique_iff {α : Type u_1} {G : } {s : } [] :
a b c, s = {a, b, c}

### Graphs without cliques #

def SimpleGraph.CliqueFree {α : Type u_1} (G : ) (n : ) :

G.CliqueFree n means that G has no n-cliques.

Instances For
theorem SimpleGraph.IsNClique.not_cliqueFree {α : Type u_1} {G : } {n : } {s : } (hG : ) :
theorem SimpleGraph.not_cliqueFree_of_top_embedding {α : Type u_1} {G : } {n : } (f : ↪g G) :
noncomputable def SimpleGraph.topEmbeddingOfNotCliqueFree {α : Type u_1} {G : } {n : } (h : ) :

An embedding of a complete graph that witnesses the fact that the graph is not clique-free.

Instances For
theorem SimpleGraph.not_cliqueFree_iff {α : Type u_1} {G : } (n : ) :
theorem SimpleGraph.cliqueFree_iff {α : Type u_1} {G : } {n : } :
theorem SimpleGraph.cliqueFree_bot {α : Type u_1} {n : } (h : 2 n) :
theorem SimpleGraph.CliqueFree.mono {α : Type u_1} {G : } {m : } {n : } (h : m n) :
theorem SimpleGraph.CliqueFree.anti {α : Type u_1} {G : } {H : } {n : } (h : G H) :
theorem SimpleGraph.cliqueFree_of_card_lt {α : Type u_1} {G : } {n : } [] (hc : ) :

See SimpleGraph.cliqueFree_of_chromaticNumber_lt for a tighter bound.

theorem SimpleGraph.cliqueFree_completeMultipartiteGraph {n : } {ι : Type u_2} [] (V : ιType u_3) (hc : ) :

A complete r-partite graph has no n-cliques for r < n.

### Set of cliques #

def SimpleGraph.cliqueSet {α : Type u_1} (G : ) (n : ) :
Set ()

The n-cliques in a graph as a set.

Instances For
theorem SimpleGraph.mem_cliqueSet_iff {α : Type u_1} (G : ) {n : } {s : } :
@[simp]
theorem SimpleGraph.cliqueSet_eq_empty_iff {α : Type u_1} (G : ) {n : } :
theorem SimpleGraph.CliqueFree.cliqueSet {α : Type u_1} (G : ) {n : } :

Alias of the reverse direction of SimpleGraph.cliqueSet_eq_empty_iff.

theorem SimpleGraph.cliqueSet_mono {α : Type u_1} {G : } {H : } {n : } (h : G H) :
theorem SimpleGraph.cliqueSet_mono' {α : Type u_1} {G : } {H : } (h : G H) :

### Finset of cliques #

def SimpleGraph.cliqueFinset {α : Type u_1} (G : ) [] [] [DecidableRel G.Adj] (n : ) :

The n-cliques in a graph as a finset.

Instances For
theorem SimpleGraph.mem_cliqueFinset_iff {α : Type u_1} (G : ) [] [] [DecidableRel G.Adj] {n : } {s : } :
@[simp]
theorem SimpleGraph.coe_cliqueFinset {α : Type u_1} (G : ) [] [] [DecidableRel G.Adj] (n : ) :
@[simp]
theorem SimpleGraph.cliqueFinset_eq_empty_iff {α : Type u_1} (G : ) [] [] [DecidableRel G.Adj] {n : } :
theorem SimpleGraph.CliqueFree.cliqueFinset {α : Type u_1} (G : ) [] [] [DecidableRel G.Adj] {n : } :

Alias of the reverse direction of SimpleGraph.cliqueFinset_eq_empty_iff.

theorem SimpleGraph.cliqueFinset_mono {α : Type u_1} {G : } (H : ) [] [] [DecidableRel G.Adj] {n : } [DecidableRel H.Adj] (h : G H) :