mathlib3 documentation

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 #

TODO #

Cliques #

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

source
theorem simple_graph.is_clique_iff {α : Type u_1} (G : simple_graph α) {s : set α} :
G.is_clique s ↔ s.pairwise G.adj
source
theorem simple_graph.is_clique_iff_induce_eq {α : Type u_1} (G : simple_graph α) {s : set α} :
G.is_clique s ↔ simple_graph.induce s G = ⊤

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

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
@[simp]
theorem simple_graph.is_clique_empty {α : Type u_1} {G : simple_graph α} :
G.is_clique ∅
source
@[simp]
theorem simple_graph.is_clique_singleton {α : Type u_1} {G : simple_graph α} (a : α) :
G.is_clique {a}
source
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
source
@[simp]
theorem simple_graph.is_clique_insert {α : Type u_1} {G : simple_graph α} {s : set α} {a : α} :
G.is_clique (has_insert.insert a s) ↔ G.is_clique s ∧ ∀ (b : α), b ∈ s → a ≠ b → G.adj a b
source
theorem simple_graph.is_clique_insert_of_not_mem {α : Type u_1} {G : simple_graph α} {s : set α} {a : α} (ha : a ∉ s) :
G.is_clique (has_insert.insert a s) ↔ G.is_clique s ∧ ∀ (b : α), b ∈ s → G.adj a b
source
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) :
G.is_clique (has_insert.insert a s)
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
@[protected]
theorem simple_graph.is_clique.map {α : Type u_1} {β : Type u_2} {G : simple_graph α} {s : set α} (h : G.is_clique s) {f : α ↪ β} :
(simple_graph.map f G).is_clique (⇑f '' s)
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
@[simp]
theorem simple_graph.is_n_clique_empty {α : Type u_1} {G : simple_graph α} {n : ℕ} :
G.is_n_clique n ∅ ↔ n = 0
source
@[simp]
theorem simple_graph.is_n_clique_singleton {α : Type u_1} {G : simple_graph α} {n : ℕ} {a : α} :
G.is_n_clique n {a} ↔ n = 1
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
@[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 : α ↪ β} :
(simple_graph.map f G).is_n_clique n (finset.map f 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
@[simp]
theorem simple_graph.is_n_clique_zero {α : Type u_1} {G : simple_graph α} {s : finset α} :
G.is_n_clique 0 s ↔ s = ∅
source
@[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}
source
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) (has_insert.insert a s)
source
theorem simple_graph.is_3_clique_triple_iff {α : Type u_1} {G : simple_graph α} {a b c : α} [decidable_eq α] :
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.is_n_clique.not_clique_free {α : Type u_1} {G : simple_graph α} {n : ℕ} {s : finset α} (hG : G.is_n_clique n s) :
¬G.clique_free n
source
theorem simple_graph.not_clique_free_of_top_embedding {α : Type u_1} {G : simple_graph α} {n : ℕ} (f : ⊤ ↪g G) :
¬G.clique_free n
source
noncomputable def simple_graph.top_embedding_of_not_clique_free {α : Type u_1} {G : simple_graph α} {n : ℕ} (h : ¬G.clique_free n) :
⊤ ↪g G

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

Equations
source
theorem simple_graph.not_clique_free_iff {α : Type u_1} {G : simple_graph α} (n : ℕ) :
¬G.clique_free n ↔ nonempty (⊤ ↪g G)
source
theorem simple_graph.clique_free_iff {α : Type u_1} {G : simple_graph α} {n : ℕ} :
G.clique_free n ↔ is_empty (⊤ ↪g G)
source
theorem simple_graph.not_clique_free_card_of_top_embedding {α : Type u_1} {G : simple_graph α} [fintype α] (f : ⊤ ↪g G) :
¬G.clique_free (fintype.card α)
source
@[simp]
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
source
theorem simple_graph.clique_free_of_card_lt {α : Type u_1} {G : simple_graph α} {n : ℕ} [fintype α] (hc : fintype.card α < n) :
G.clique_free n

See simple_graph.clique_free_chromatic_number_succ for a tighter bound.

source
@[simp]
theorem simple_graph.clique_free_two {α : Type u_1} {G : simple_graph α} :
G.clique_free 2 ↔ G = ⊥
source
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
source
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) :
G.clique_free_on s₁ n
source
theorem simple_graph.clique_free_on.mono {α : Type u_1} (G : simple_graph α) {s : set α} {m n : ℕ} (hmn : m ≤ n) (hG : G.clique_free_on s m) :
G.clique_free_on s n
source
theorem simple_graph.clique_free_on.anti {α : Type u_1} (G H : simple_graph α) {s : set α} {n : ℕ} (hGH : G ≤ H) (hH : H.clique_free_on s n) :
G.clique_free_on s n
source
@[simp]
theorem simple_graph.clique_free_on_empty {α : Type u_1} (G : simple_graph α) {n : ℕ} :
G.clique_free_on ∅ n ↔ n ≠ 0
source
@[simp]
theorem simple_graph.clique_free_on_singleton {α : Type u_1} (G : simple_graph α) {a : α} {n : ℕ} :
G.clique_free_on {a} n ↔ 1 < n
source
@[simp]
theorem simple_graph.clique_free_on_univ {α : Type u_1} (G : simple_graph α) {n : ℕ} :
G.clique_free_on set.univ n ↔ G.clique_free n
source
@[protected]
theorem simple_graph.clique_free.clique_free_on {α : Type u_1} (G : simple_graph α) {s : set α} {n : ℕ} (hG : G.clique_free n) :
G.clique_free_on s n
source
theorem simple_graph.clique_free_on_of_card_lt {α : Type u_1} (G : simple_graph α) {n : ℕ} {s : finset α} (h : s.card < n) :
G.clique_free_on ↑s n
source
@[simp]
theorem simple_graph.clique_free_on_two {α : Type u_1} (G : simple_graph α) {s : set α} :
G.clique_free_on s 2 ↔ s.pairwise G.adjᶜ
source
theorem simple_graph.clique_free_on.of_succ {α : Type u_1} (G : simple_graph α) {s : set α} {a : α} {n : ℕ} (hs : G.clique_free_on s (n + 1)) (ha : a ∈ s) :
G.clique_free_on (s ∩ G.neighbor_set a) n

Set of cliques #

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

The n-cliques in a graph as a set.

Equations
source
@[simp]
theorem simple_graph.mem_clique_set_iff {α : Type u_1} (G : simple_graph α) {n : ℕ} {s : finset α} :
s ∈ G.clique_set n ↔ G.is_n_clique n s
source
@[simp]
theorem simple_graph.clique_set_eq_empty_iff {α : Type u_1} (G : simple_graph α) {n : ℕ} :
G.clique_set n = ∅ ↔ G.clique_free n
source
@[protected]
theorem simple_graph.clique_free.clique_set {α : Type u_1} {G : simple_graph α} {n : ℕ} :
G.clique_free n → G.clique_set n = ∅
source
theorem simple_graph.clique_set_mono {α : Type u_1} {G H : simple_graph α} {n : ℕ} (h : G ≤ H) :
G.clique_set n ⊆ H.clique_set n
source
theorem simple_graph.clique_set_mono' {α : Type u_1} {G H : simple_graph α} (h : G ≤ H) :
G.clique_set ≤ H.clique_set
source
@[simp]
theorem simple_graph.clique_set_zero {α : Type u_1} (G : simple_graph α) :
G.clique_set 0 = {∅}
source
@[simp]
theorem simple_graph.clique_set_one {α : Type u_1} (G : simple_graph α) :
G.clique_set 1 = set.range has_singleton.singleton
source
@[simp]
theorem simple_graph.clique_set_bot {α : Type u_1} {n : ℕ} (hn : 1 < n) :
⊥.clique_set n = ∅
source
@[simp]
theorem simple_graph.clique_set_map {α : Type u_1} {β : Type u_2} {n : ℕ} (hn : n ≠ 1) (G : simple_graph α) (f : α ↪ β) :
(simple_graph.map f G).clique_set n = finset.map f '' G.clique_set n
source
@[simp]
theorem simple_graph.clique_set_map_of_equiv {α : Type u_1} {β : Type u_2} (G : simple_graph α) (e : α ≃ β) (n : ℕ) :
(simple_graph.map e.to_embedding G).clique_set n = finset.map e.to_embedding '' G.clique_set 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
@[simp]
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, norm_cast]
theorem simple_graph.coe_clique_finset {α : Type u_1} (G : simple_graph α) [fintype α] [decidable_eq α] [decidable_rel G.adj] (n : ℕ) :
↑(G.clique_finset n) = G.clique_set n
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.card_clique_finset_le {α : Type u_1} {G : simple_graph α} [fintype α] [decidable_eq α] [decidable_rel G.adj] {n : ℕ} :
(G.clique_finset n).card ≤ (fintype.card α).choose n
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
source
@[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) :
(simple_graph.map f G).clique_finset n = finset.map {to_fun := finset.map f, inj' := _} (G.clique_finset n)
source
@[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 : ℕ) :
(simple_graph.map e.to_embedding G).clique_finset n = finset.map {to_fun := finset.map e.to_embedding, inj' := _} (G.clique_finset n)