# mathlib3documentation

combinatorics.simple_graph.clique

# Graph cliques #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

## Main declarations #

• simple_graph.is_clique: Predicate for a set of vertices to be a clique.
• simple_graph.is_n_clique: Predicate for a set of vertices to be a n-clique.
• simple_graph.clique_finset: Finset of n-cliques of a graph.
• simple_graph.clique_free: Predicate for a graph to have no n-cliques.

## TODO #

• Clique numbers
• Dualise all the API to get independent sets

### Cliques #

@[reducible]
def simple_graph.is_clique {α : Type u_1} (G : simple_graph α) (s : set α) :
Prop

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

theorem simple_graph.is_clique_iff {α : Type u_1} (G : simple_graph α) {s : set α} :
theorem simple_graph.is_clique_iff_induce_eq {α : Type u_1} (G : simple_graph α) {s : set α} :

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

@[protected, instance]
Equations
@[simp]
theorem simple_graph.is_clique_empty {α : Type u_1} {G : simple_graph α} :
@[simp]
theorem simple_graph.is_clique_singleton {α : Type u_1} {G : simple_graph α} (a : α) :
G.is_clique {a}
theorem simple_graph.is_clique_pair {α : Type u_1} {G : simple_graph α} {a b : α} :
G.is_clique {a, b} a b G.adj a b
@[simp]
theorem simple_graph.is_clique_insert {α : Type u_1} {G : simple_graph α} {s : set α} {a : α} :
G.is_clique s) G.is_clique s (b : α), b s a b G.adj a b
theorem simple_graph.is_clique_insert_of_not_mem {α : Type u_1} {G : simple_graph α} {s : set α} {a : α} (ha : a s) :
G.is_clique s) G.is_clique s (b : α), b s G.adj a b
theorem simple_graph.is_clique.insert {α : Type u_1} {G : simple_graph α} {s : set α} {a : α} (hs : G.is_clique s) (h : (b : α), b s a b G.adj a b) :
theorem simple_graph.is_clique.mono {α : Type u_1} {G H : simple_graph α} {s : set α} (h : G H) :
theorem simple_graph.is_clique.subset {α : Type u_1} {G : simple_graph α} {s t : set α} (h : t s) :
@[protected]
theorem simple_graph.is_clique.map {α : Type u_1} {β : Type u_2} {G : simple_graph α} {s : set α} (h : G.is_clique s) {f : α β} :
G).is_clique (f '' s)
@[simp]
theorem simple_graph.is_clique_bot_iff {α : Type u_1} {s : set α} :
theorem simple_graph.is_clique.subsingleton {α : Type u_1} {s : set α} :

Alias of the forward direction of simple_graph.is_clique_bot_iff.

### n-cliques #

structure simple_graph.is_n_clique {α : Type u_1} (G : simple_graph α) (n : ) (s : finset α) :
Prop

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

Instances for simple_graph.is_n_clique
theorem simple_graph.is_n_clique_iff {α : Type u_1} (G : simple_graph α) {n : } {s : finset α} :
@[protected, instance]
Equations
@[simp]
theorem simple_graph.is_n_clique_empty {α : Type u_1} {G : simple_graph α} {n : } :
@[simp]
theorem simple_graph.is_n_clique_singleton {α : Type u_1} {G : simple_graph α} {n : } {a : α} :
G.is_n_clique n {a} n = 1
theorem simple_graph.is_n_clique.mono {α : Type u_1} {G H : simple_graph α} {n : } {s : finset α} (h : G H) :
@[protected]
theorem simple_graph.is_n_clique.map {α : Type u_1} {β : Type u_2} {G : simple_graph α} {n : } {s : finset α} (h : G.is_n_clique n s) {f : α β} :
G).is_n_clique n s)
@[simp]
theorem simple_graph.is_n_clique_bot_iff {α : Type u_1} {n : } {s : finset α} :
s n 1 s.card = n
@[simp]
theorem simple_graph.is_n_clique_zero {α : Type u_1} {G : simple_graph α} {s : finset α} :
@[simp]
theorem simple_graph.is_n_clique_one {α : Type u_1} {G : simple_graph α} {s : finset α} :
G.is_n_clique 1 s (a : α), s = {a}
theorem simple_graph.is_n_clique.insert {α : Type u_1} {G : simple_graph α} {n : } {s : finset α} {a : α} [decidable_eq α] (hs : G.is_n_clique n s) (h : (b : α), b s G.adj a b) :
G.is_n_clique (n + 1) s)
theorem simple_graph.is_3_clique_triple_iff {α : Type u_1} {G : simple_graph α} {a b c : α} [decidable_eq α] :
theorem simple_graph.is_3_clique_iff {α : Type u_1} {G : simple_graph α} {s : finset α} [decidable_eq α] :
G.is_n_clique 3 s (a b c : α), G.adj a b G.adj a c G.adj b c s = {a, b, c}

### Graphs without cliques #

def simple_graph.clique_free {α : Type u_1} (G : simple_graph α) (n : ) :
Prop

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

Equations
theorem simple_graph.is_n_clique.not_clique_free {α : Type u_1} {G : simple_graph α} {n : } {s : finset α} (hG : G.is_n_clique n s) :
noncomputable def simple_graph.top_embedding_of_not_clique_free {α : Type u_1} {G : simple_graph α} {n : } (h : ¬G.clique_free n) :

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

Equations
theorem simple_graph.clique_free_iff {α : Type u_1} {G : simple_graph α} {n : } :
@[simp]
theorem simple_graph.clique_free_bot {α : Type u_1} {n : } (h : 2 n) :
theorem simple_graph.clique_free.mono {α : Type u_1} {G : simple_graph α} {m n : } (h : m n) :
theorem simple_graph.clique_free.anti {α : Type u_1} {G H : simple_graph α} {n : } (h : G H) :
theorem simple_graph.clique_free_of_card_lt {α : Type u_1} {G : simple_graph α} {n : } [fintype α] (hc : < n) :

See simple_graph.clique_free_chromatic_number_succ for a tighter bound.

@[simp]
theorem simple_graph.clique_free_two {α : Type u_1} {G : simple_graph α} :
def simple_graph.clique_free_on {α : Type u_1} (G : simple_graph α) (s : set α) (n : ) :
Prop

G.clique_free_on s n means that G has no n-cliques contained in s.

Equations
theorem simple_graph.clique_free_on.subset {α : Type u_1} (G : simple_graph α) {s₁ s₂ : set α} {n : } (hs : s₁ s₂) (h₂ : G.clique_free_on s₂ n) :
theorem simple_graph.clique_free_on.mono {α : Type u_1} (G : simple_graph α) {s : set α} {m n : } (hmn : m n) (hG : m) :
n
theorem simple_graph.clique_free_on.anti {α : Type u_1} (G H : simple_graph α) {s : set α} {n : } (hGH : G H) (hH : n) :
n
@[simp]
theorem simple_graph.clique_free_on_empty {α : Type u_1} (G : simple_graph α) {n : } :
n n 0
@[simp]
theorem simple_graph.clique_free_on_singleton {α : Type u_1} (G : simple_graph α) {a : α} {n : } :
G.clique_free_on {a} n 1 < n
@[simp]
theorem simple_graph.clique_free_on_univ {α : Type u_1} (G : simple_graph α) {n : } :
@[protected]
theorem simple_graph.clique_free.clique_free_on {α : Type u_1} (G : simple_graph α) {s : set α} {n : } (hG : G.clique_free n) :
n
theorem simple_graph.clique_free_on_of_card_lt {α : Type u_1} (G : simple_graph α) {n : } {s : finset α} (h : s.card < n) :
n
@[simp]
theorem simple_graph.clique_free_on_two {α : Type u_1} (G : simple_graph α) {s : set α} :
theorem simple_graph.clique_free_on.of_succ {α : Type u_1} (G : simple_graph α) {s : set α} {a : α} {n : } (hs : (n + 1)) (ha : a s) :

### Set of cliques #

def simple_graph.clique_set {α : Type u_1} (G : simple_graph α) (n : ) :
set (finset α)

The n-cliques in a graph as a set.

Equations
@[simp]
theorem simple_graph.mem_clique_set_iff {α : Type u_1} (G : simple_graph α) {n : } {s : finset α} :
@[simp]
@[protected]
theorem simple_graph.clique_free.clique_set {α : Type u_1} {G : simple_graph α} {n : } :
theorem simple_graph.clique_set_mono {α : Type u_1} {G H : simple_graph α} {n : } (h : G H) :
theorem simple_graph.clique_set_mono' {α : Type u_1} {G H : simple_graph α} (h : G H) :
@[simp]
theorem simple_graph.clique_set_zero {α : Type u_1} (G : simple_graph α) :
@[simp]
theorem simple_graph.clique_set_one {α : Type u_1} (G : simple_graph α) :
@[simp]
theorem simple_graph.clique_set_bot {α : Type u_1} {n : } (hn : 1 < n) :
@[simp]
theorem simple_graph.clique_set_map {α : Type u_1} {β : Type u_2} {n : } (hn : n 1) (G : simple_graph α) (f : α β) :
@[simp]
theorem simple_graph.clique_set_map_of_equiv {α : Type u_1} {β : Type u_2} (G : simple_graph α) (e : α β) (n : ) :
=

### Finset of cliques #

def simple_graph.clique_finset {α : Type u_1} (G : simple_graph α) [fintype α] [decidable_eq α] [decidable_rel G.adj] (n : ) :

The n-cliques in a graph as a finset.

Equations
@[simp]
theorem simple_graph.mem_clique_finset_iff {α : Type u_1} (G : simple_graph α) [fintype α] [decidable_eq α] [decidable_rel G.adj] {n : } {s : finset α} :
@[simp, norm_cast]
@[protected]

Alias of the reverse direction of simple_graph.clique_finset_eq_empty_iff.

theorem simple_graph.clique_finset_mono {α : Type u_1} {G : simple_graph α} (H : simple_graph α) [fintype α] [decidable_eq α] [decidable_rel G.adj] {n : } [decidable_rel H.adj] (h : G H) :
@[simp]
theorem simple_graph.clique_finset_map {α : Type u_1} {β : Type u_2} (G : simple_graph α) [fintype α] [decidable_eq α] [decidable_rel G.adj] {n : } [fintype β] [decidable_eq β] (f : α β) (hn : n 1) :
n = finset.map {to_fun := , inj' := _} (G.clique_finset n)
@[simp]
theorem simple_graph.clique_finset_map_of_equiv {α : Type u_1} {β : Type u_2} (G : simple_graph α) [fintype α] [decidable_eq α] [decidable_rel G.adj] [fintype β] [decidable_eq β] (e : α β) (n : ) :