mathlib documentation

combinatorics.simple_graph.clique

Graph cliques #

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

Main declarations #

TODO #

Cliques #

source
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.

source
theorem simple_graph.is_clique_iff {α : Type u_1} (G : simple_graph α) {s : set α} :
G.is_clique s ↔ s.pairwise G.adj
source
@[protected, instance]
def simple_graph.is_clique.decidable {α : Type u_1} (G : simple_graph α) [decidable_eq α] [decidable_rel G.adj] {s : finset α} :
decidable (G.is_clique ↑s)
Equations
source
theorem simple_graph.is_clique.mono {α : Type u_1} {G H : simple_graph α} {s : set α} (h : G ≤ H) :
G.is_clique s → H.is_clique s
source
theorem simple_graph.is_clique.subset {α : Type u_1} {G : simple_graph α} {s t : set α} (h : t ⊆ s) :
G.is_clique s → G.is_clique t
source
@[simp]
theorem simple_graph.is_clique_bot_iff {α : Type u_1} {s : set α} :
⊥.is_clique s ↔ s.subsingleton
source
theorem simple_graph.is_clique.subsingleton {α : Type u_1} {s : set α} :
⊥.is_clique s → s.subsingleton

Alias of the forward direction of simple_graph.is_clique_bot_iff`.

n-cliques #

source
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
source
theorem simple_graph.is_n_clique_iff {α : Type u_1} (G : simple_graph α) {n : ℕ} {s : finset α} :
G.is_n_clique n s ↔ G.is_clique ↑s ∧ s.card = n
source
@[protected, instance]
def simple_graph.is_n_clique.decidable {α : Type u_1} (G : simple_graph α) [decidable_eq α] [decidable_rel G.adj] {n : ℕ} {s : finset α} :
decidable (G.is_n_clique n s)
Equations
source
theorem simple_graph.is_n_clique.mono {α : Type u_1} {G H : simple_graph α} {n : ℕ} {s : finset α} (h : G ≤ H) :
G.is_n_clique n s → H.is_n_clique n s
source
@[simp]
theorem simple_graph.is_n_clique_bot_iff {α : Type u_1} {n : ℕ} {s : finset α} :
⊥.is_n_clique n s ↔ n ≤ 1 ∧ s.card = n
source
theorem simple_graph.is_3_clique_triple_iff {α : Type u_1} {G : simple_graph α} [decidable_eq α] {a b c : α} :
G.is_n_clique 3 {a, b, c} ↔ G.adj a b ∧ G.adj a c ∧ G.adj b c
source
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 #

source
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
source
theorem simple_graph.clique_free_bot {α : Type u_1} {n : ℕ} (h : 2 ≤ n) :
⊥.clique_free n
source
theorem simple_graph.clique_free.mono {α : Type u_1} {G : simple_graph α} {m n : ℕ} (h : m ≤ n) :
G.clique_free m → G.clique_free n
source
theorem simple_graph.clique_free.anti {α : Type u_1} {G H : simple_graph α} {n : ℕ} (h : G ≤ H) :
H.clique_free n → G.clique_free n

Finset of cliques #

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

The n-cliques in a graph as a finset.

Equations
source
theorem simple_graph.mem_clique_finset_iff {α : Type u_1} (G : simple_graph α) [fintype α] [decidable_eq α] [decidable_rel G.adj] {n : ℕ} (s : finset α) :
s ∈ G.clique_finset n ↔ G.is_n_clique n s
source
@[simp]
theorem simple_graph.clique_finset_eq_empty_iff {α : Type u_1} (G : simple_graph α) [fintype α] [decidable_eq α] [decidable_rel G.adj] {n : ℕ} :
G.clique_finset n = ∅ ↔ G.clique_free n
source
@[protected]
theorem simple_graph.clique_free.clique_finset {α : Type u_1} (G : simple_graph α) [fintype α] [decidable_eq α] [decidable_rel G.adj] {n : ℕ} :
G.clique_free n → G.clique_finset n = ∅

Alias of the reverse direction of simple_graph.clique_finset_eq_empty_iff`.

source
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) :
G.clique_finset n ⊆ H.clique_finset n