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
• Dualise all the API to get independent sets

Cliques

@[inline, reducible]

abbrev SimpleGraph.IsClique {α : Type u_1} (G : SimpleGraph α) (s : Set α) : Prop

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

Equations

• SimpleGraph.IsClique G s = Set.Pairwise s G.Adj

theorem SimpleGraph.isClique_iff {α : Type u_1} (G : SimpleGraph α) {s : Set α} : SimpleGraph.IsClique G s ↔ Set.Pairwise s G.Adj

theorem SimpleGraph.isClique_iff_induce_eq {α : Type u_1} (G : SimpleGraph α) {s : Set α} : SimpleGraph.IsClique G s ↔ SimpleGraph.induce s G = ⊤

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

instance SimpleGraph.instDecidableIsCliqueToSet {α : Type u_1} (G : SimpleGraph α) [DecidableEq α] [DecidableRel G.Adj] {s : Finset α} : Decidable (SimpleGraph.IsClique G ↑s)

Equations

• SimpleGraph.instDecidableIsCliqueToSet G = decidable_of_iff' (Set.Pairwise (↑s) G.Adj) (_ : SimpleGraph.IsClique G ↑s ↔ Set.Pairwise (↑s) G.Adj)

theorem SimpleGraph.isClique_empty {α : Type u_1} {G : SimpleGraph α} : SimpleGraph.IsClique G ∅

theorem SimpleGraph.isClique_singleton {α : Type u_1} {G : SimpleGraph α} (a : α) : SimpleGraph.IsClique G {a}

theorem SimpleGraph.isClique_pair {α : Type u_1} {G : SimpleGraph α} {a : α} {b : α} : SimpleGraph.IsClique G {a, b} ↔ a ≠ b → G.Adj a b

@[simp]

theorem SimpleGraph.isClique_insert {α : Type u_1} {G : SimpleGraph α} {s : Set α} {a : α} : SimpleGraph.IsClique G (insert a s) ↔ SimpleGraph.IsClique G s ∧ ∀ b ∈ s, a ≠ b → G.Adj a b

theorem SimpleGraph.isClique_insert_of_not_mem {α : Type u_1} {G : SimpleGraph α} {s : Set α} {a : α} (ha : a ∉ s) : SimpleGraph.IsClique G (insert a s) ↔ SimpleGraph.IsClique G s ∧ ∀ b ∈ s, G.Adj a b

theorem SimpleGraph.IsClique.insert {α : Type u_1} {G : SimpleGraph α} {s : Set α} {a : α} (hs : SimpleGraph.IsClique G s) (h : ∀ b ∈ s, a ≠ b → G.Adj a b) : SimpleGraph.IsClique G (insert a s)

theorem SimpleGraph.IsClique.mono {α : Type u_1} {G : SimpleGraph α} {H : SimpleGraph α} {s : Set α} (h : G ≤ H) : SimpleGraph.IsClique G s → SimpleGraph.IsClique H s

theorem SimpleGraph.IsClique.subset {α : Type u_1} {G : SimpleGraph α} {s : Set α} {t : Set α} (h : t ⊆ s) : SimpleGraph.IsClique G s → SimpleGraph.IsClique G t

theorem SimpleGraph.IsClique.map {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {s : Set α} (h : SimpleGraph.IsClique G s) {f : α ↪ β} : SimpleGraph.IsClique (SimpleGraph.map f G) (⇑f '' s)

@[simp]

theorem SimpleGraph.isClique_bot_iff {α : Type u_1} {s : Set α} : SimpleGraph.IsClique ⊥ s ↔ Set.Subsingleton s

theorem SimpleGraph.IsClique.subsingleton {α : Type u_1} {s : Set α} : SimpleGraph.IsClique ⊥ s → Set.Subsingleton s

Alias of the forward direction of SimpleGraph.isClique_bot_iff.

n-cliques

structure SimpleGraph.IsNClique {α : Type u_1} (G : SimpleGraph α) (n : ℕ) (s : Finset α) : Prop

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

• clique : SimpleGraph.IsClique G ↑s
• card_eq : s.card = n

theorem SimpleGraph.isNClique_iff {α : Type u_1} (G : SimpleGraph α) {n : ℕ} {s : Finset α} : SimpleGraph.IsNClique G n s ↔ SimpleGraph.IsClique G ↑s ∧ s.card = n

instance SimpleGraph.instDecidableIsNClique {α : Type u_1} (G : SimpleGraph α) [DecidableEq α] [DecidableRel G.Adj] {n : ℕ} {s : Finset α} : Decidable (SimpleGraph.IsNClique G n s)

Equations

• SimpleGraph.instDecidableIsNClique G = decidable_of_iff' (SimpleGraph.IsClique G ↑s ∧ s.card = n) (_ : SimpleGraph.IsNClique G n s ↔ SimpleGraph.IsClique G ↑s ∧ s.card = n)

@[simp]

theorem SimpleGraph.isNClique_empty {α : Type u_1} {G : SimpleGraph α} {n : ℕ} : SimpleGraph.IsNClique G n ∅ ↔ n = 0

@[simp]

theorem SimpleGraph.isNClique_singleton {α : Type u_1} {G : SimpleGraph α} {n : ℕ} {a : α} : SimpleGraph.IsNClique G n {a} ↔ n = 1

theorem SimpleGraph.IsNClique.mono {α : Type u_1} {G : SimpleGraph α} {H : SimpleGraph α} {n : ℕ} {s : Finset α} (h : G ≤ H) : SimpleGraph.IsNClique G n s → SimpleGraph.IsNClique H n s

theorem SimpleGraph.IsNClique.map {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {n : ℕ} {s : Finset α} (h : SimpleGraph.IsNClique G n s) {f : α ↪ β} : SimpleGraph.IsNClique (SimpleGraph.map f G) n (Finset.map f s)

@[simp]

theorem SimpleGraph.isNClique_bot_iff {α : Type u_1} {n : ℕ} {s : Finset α} : SimpleGraph.IsNClique ⊥ n s ↔ n ≤ 1 ∧ s.card = n

@[simp]

theorem SimpleGraph.isNClique_zero {α : Type u_1} {G : SimpleGraph α} {s : Finset α} : SimpleGraph.IsNClique G 0 s ↔ s = ∅

@[simp]

theorem SimpleGraph.isNClique_one {α : Type u_1} {G : SimpleGraph α} {s : Finset α} : SimpleGraph.IsNClique G 1 s ↔ ∃ (a : α), s = {a}

theorem SimpleGraph.IsNClique.insert {α : Type u_1} {G : SimpleGraph α} {n : ℕ} {s : Finset α} {a : α} [DecidableEq α] (hs : SimpleGraph.IsNClique G n s) (h : ∀ b ∈ s, G.Adj a b) : SimpleGraph.IsNClique G (n + 1) (insert a s)

theorem SimpleGraph.is3Clique_triple_iff {α : Type u_1} {G : SimpleGraph α} {a : α} {b : α} {c : α} [DecidableEq α] : SimpleGraph.IsNClique G 3 {a, b, c} ↔ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c

theorem SimpleGraph.is3Clique_iff {α : Type u_1} {G : SimpleGraph α} {s : Finset α} [DecidableEq α] : SimpleGraph.IsNClique G 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 SimpleGraph.CliqueFree {α : Type u_1} (G : SimpleGraph α) (n : ℕ) : Prop

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

Equations

• SimpleGraph.CliqueFree G n = ∀ (t : Finset α), ¬SimpleGraph.IsNClique G n t

theorem SimpleGraph.IsNClique.not_cliqueFree {α : Type u_1} {G : SimpleGraph α} {n : ℕ} {s : Finset α} (hG : SimpleGraph.IsNClique G n s) : ¬SimpleGraph.CliqueFree G n

theorem SimpleGraph.not_cliqueFree_of_top_embedding {α : Type u_1} {G : SimpleGraph α} {n : ℕ} (f : ⊤ ↪g G) : ¬SimpleGraph.CliqueFree G n

noncomputable def SimpleGraph.topEmbeddingOfNotCliqueFree {α : Type u_1} {G : SimpleGraph α} {n : ℕ} (h : ¬SimpleGraph.CliqueFree G n) : ⊤ ↪g G

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

Equations

• One or more equations did not get rendered due to their size.

theorem SimpleGraph.not_cliqueFree_iff {α : Type u_1} {G : SimpleGraph α} (n : ℕ) : ¬SimpleGraph.CliqueFree G n ↔ Nonempty (⊤ ↪g G)

theorem SimpleGraph.cliqueFree_iff {α : Type u_1} {G : SimpleGraph α} {n : ℕ} : SimpleGraph.CliqueFree G n ↔ IsEmpty (⊤ ↪g G)

theorem SimpleGraph.not_cliqueFree_card_of_top_embedding {α : Type u_1} {G : SimpleGraph α} [Fintype α] (f : ⊤ ↪g G) : ¬SimpleGraph.CliqueFree G (Fintype.card α)

@[simp]

theorem SimpleGraph.cliqueFree_bot {α : Type u_1} {n : ℕ} (h : 2 ≤ n) : SimpleGraph.CliqueFree ⊥ n

theorem SimpleGraph.CliqueFree.mono {α : Type u_1} {G : SimpleGraph α} {m : ℕ} {n : ℕ} (h : m ≤ n) : SimpleGraph.CliqueFree G m → SimpleGraph.CliqueFree G n

theorem SimpleGraph.CliqueFree.anti {α : Type u_1} {G : SimpleGraph α} {H : SimpleGraph α} {n : ℕ} (h : G ≤ H) : SimpleGraph.CliqueFree H n → SimpleGraph.CliqueFree G n

theorem SimpleGraph.CliqueFree.comap {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {n : ℕ} {H : SimpleGraph β} (f : H ↪g G) : SimpleGraph.CliqueFree G n → SimpleGraph.CliqueFree H n

If a graph is cliquefree, any graph that embeds into it is also cliquefree.

theorem SimpleGraph.cliqueFree_of_card_lt {α : Type u_1} {G : SimpleGraph α} {n : ℕ} [Fintype α] (hc : Fintype.card α < n) : SimpleGraph.CliqueFree G n

See SimpleGraph.cliqueFree_of_chromaticNumber_lt for a tighter bound.

theorem SimpleGraph.cliqueFree_completeMultipartiteGraph {n : ℕ} {ι : Type u_3} [Fintype ι] (V : ι → Type u_4) (hc : Fintype.card ι < n) : SimpleGraph.CliqueFree (SimpleGraph.completeMultipartiteGraph V) n

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

theorem SimpleGraph.CliqueFree.replaceVertex {α : Type u_1} {G : SimpleGraph α} {n : ℕ} [DecidableEq α] (h : SimpleGraph.CliqueFree G n) (s : α) (t : α) : SimpleGraph.CliqueFree (SimpleGraph.replaceVertex G s t) n

Clique-freeness is preserved by replaceVertex.

@[simp]

theorem SimpleGraph.cliqueFree_two {α : Type u_1} {G : SimpleGraph α} : SimpleGraph.CliqueFree G 2 ↔ G = ⊥

theorem SimpleGraph.CliqueFree.addEdge {α : Type u_1} {G : SimpleGraph α} {n : ℕ} (h : SimpleGraph.CliqueFree G n) (v : α) (w : α) : SimpleGraph.CliqueFree (SimpleGraph.addEdge G v w) (n + 1)

Adding an edge increases the clique number by at most one.

def SimpleGraph.CliqueFreeOn {α : Type u_1} (G : SimpleGraph α) (s : Set α) (n : ℕ) : Prop

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

Equations

• SimpleGraph.CliqueFreeOn G s n = ∀ ⦃t : Finset α⦄, ↑t ⊆ s → ¬SimpleGraph.IsNClique G n t

theorem SimpleGraph.CliqueFreeOn.subset {α : Type u_1} (G : SimpleGraph α) {s₁ : Set α} {s₂ : Set α} {n : ℕ} (hs : s₁ ⊆ s₂) (h₂ : SimpleGraph.CliqueFreeOn G s₂ n) : SimpleGraph.CliqueFreeOn G s₁ n

theorem SimpleGraph.CliqueFreeOn.mono {α : Type u_1} (G : SimpleGraph α) {s : Set α} {m : ℕ} {n : ℕ} (hmn : m ≤ n) (hG : SimpleGraph.CliqueFreeOn G s m) : SimpleGraph.CliqueFreeOn G s n

theorem SimpleGraph.CliqueFreeOn.anti {α : Type u_1} (G : SimpleGraph α) (H : SimpleGraph α) {s : Set α} {n : ℕ} (hGH : G ≤ H) (hH : SimpleGraph.CliqueFreeOn H s n) : SimpleGraph.CliqueFreeOn G s n

@[simp]

theorem SimpleGraph.cliqueFreeOn_empty {α : Type u_1} (G : SimpleGraph α) {n : ℕ} : SimpleGraph.CliqueFreeOn G ∅ n ↔ n ≠ 0

@[simp]

theorem SimpleGraph.cliqueFreeOn_singleton {α : Type u_1} (G : SimpleGraph α) {a : α} {n : ℕ} : SimpleGraph.CliqueFreeOn G {a} n ↔ 1 < n

@[simp]

theorem SimpleGraph.cliqueFreeOn_univ {α : Type u_1} (G : SimpleGraph α) {n : ℕ} : SimpleGraph.CliqueFreeOn G Set.univ n ↔ SimpleGraph.CliqueFree G n

theorem SimpleGraph.CliqueFree.cliqueFreeOn {α : Type u_1} (G : SimpleGraph α) {s : Set α} {n : ℕ} (hG : SimpleGraph.CliqueFree G n) : SimpleGraph.CliqueFreeOn G s n

theorem SimpleGraph.cliqueFreeOn_of_card_lt {α : Type u_1} (G : SimpleGraph α) {n : ℕ} {s : Finset α} (h : s.card < n) : SimpleGraph.CliqueFreeOn G (↑s) n

@[simp]

theorem SimpleGraph.cliqueFreeOn_two {α : Type u_1} (G : SimpleGraph α) {s : Set α} : SimpleGraph.CliqueFreeOn G s 2 ↔ Set.Pairwise s G.Adjᶜ

theorem SimpleGraph.CliqueFreeOn.of_succ {α : Type u_1} (G : SimpleGraph α) {s : Set α} {a : α} {n : ℕ} (hs : SimpleGraph.CliqueFreeOn G s (n + 1)) (ha : a ∈ s) : SimpleGraph.CliqueFreeOn G (s ∩ SimpleGraph.neighborSet G a) n

Set of cliques

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

The n-cliques in a graph as a set.

Equations

• SimpleGraph.cliqueSet G n = {s : Finset α | SimpleGraph.IsNClique G n s}

@[simp]

theorem SimpleGraph.mem_cliqueSet_iff {α : Type u_1} {G : SimpleGraph α} {n : ℕ} {s : Finset α} : s ∈ SimpleGraph.cliqueSet G n ↔ SimpleGraph.IsNClique G n s

@[simp]

theorem SimpleGraph.cliqueSet_eq_empty_iff {α : Type u_1} {G : SimpleGraph α} {n : ℕ} : SimpleGraph.cliqueSet G n = ∅ ↔ SimpleGraph.CliqueFree G n

theorem SimpleGraph.CliqueFree.cliqueSet {α : Type u_1} {G : SimpleGraph α} {n : ℕ} : SimpleGraph.CliqueFree G n → SimpleGraph.cliqueSet G n = ∅

Alias of the reverse direction of SimpleGraph.cliqueSet_eq_empty_iff.

theorem SimpleGraph.cliqueSet_mono {α : Type u_1} {G : SimpleGraph α} {H : SimpleGraph α} {n : ℕ} (h : G ≤ H) : SimpleGraph.cliqueSet G n ⊆ SimpleGraph.cliqueSet H n

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

@[simp]

theorem SimpleGraph.cliqueSet_zero {α : Type u_1} (G : SimpleGraph α) : SimpleGraph.cliqueSet G 0 = {∅}

@[simp]

theorem SimpleGraph.cliqueSet_one {α : Type u_1} (G : SimpleGraph α) : SimpleGraph.cliqueSet G 1 = Set.range singleton

@[simp]

theorem SimpleGraph.cliqueSet_bot {α : Type u_1} {n : ℕ} (hn : 1 < n) : SimpleGraph.cliqueSet ⊥ n = ∅

@[simp]

theorem SimpleGraph.cliqueSet_map {α : Type u_1} {β : Type u_2} {n : ℕ} (hn : n ≠ 1) (G : SimpleGraph α) (f : α ↪ β) : SimpleGraph.cliqueSet (SimpleGraph.map f G) n = Finset.map f '' SimpleGraph.cliqueSet G n

@[simp]

theorem SimpleGraph.cliqueSet_map_of_equiv {α : Type u_1} {β : Type u_2} (G : SimpleGraph α) (e : α ≃ β) (n : ℕ) : SimpleGraph.cliqueSet (SimpleGraph.map (Equiv.toEmbedding e) G) n = Finset.map (Equiv.toEmbedding e) '' SimpleGraph.cliqueSet G n

Finset of cliques

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

The n-cliques in a graph as a finset.

Equations

• SimpleGraph.cliqueFinset G n = Finset.filter (SimpleGraph.IsNClique G n) Finset.univ

@[simp]

theorem SimpleGraph.mem_cliqueFinset_iff {α : Type u_1} {G : SimpleGraph α} [Fintype α] [DecidableEq α] [DecidableRel G.Adj] {n : ℕ} {s : Finset α} : s ∈ SimpleGraph.cliqueFinset G n ↔ SimpleGraph.IsNClique G n s

@[simp]

theorem SimpleGraph.coe_cliqueFinset {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableEq α] [DecidableRel G.Adj] (n : ℕ) : ↑(SimpleGraph.cliqueFinset G n) = SimpleGraph.cliqueSet G n

@[simp]

theorem SimpleGraph.cliqueFinset_eq_empty_iff {α : Type u_1} {G : SimpleGraph α} [Fintype α] [DecidableEq α] [DecidableRel G.Adj] {n : ℕ} : SimpleGraph.cliqueFinset G n = ∅ ↔ SimpleGraph.CliqueFree G n

theorem SimpleGraph.CliqueFree.cliqueFinset {α : Type u_1} {G : SimpleGraph α} [Fintype α] [DecidableEq α] [DecidableRel G.Adj] {n : ℕ} : SimpleGraph.CliqueFree G n → SimpleGraph.cliqueFinset G n = ∅

Alias of the reverse direction of SimpleGraph.cliqueFinset_eq_empty_iff.

theorem SimpleGraph.card_cliqueFinset_le {α : Type u_1} {G : SimpleGraph α} [Fintype α] [DecidableEq α] [DecidableRel G.Adj] {n : ℕ} : (SimpleGraph.cliqueFinset G n).card ≤ Nat.choose (Fintype.card α) n

theorem SimpleGraph.cliqueFinset_mono {α : Type u_1} {G : SimpleGraph α} (H : SimpleGraph α) [Fintype α] [DecidableEq α] [DecidableRel G.Adj] {n : ℕ} [DecidableRel H.Adj] (h : G ≤ H) : SimpleGraph.cliqueFinset G n ⊆ SimpleGraph.cliqueFinset H n

@[simp]

theorem SimpleGraph.cliqueFinset_map {α : Type u_1} {β : Type u_2} (G : SimpleGraph α) [Fintype α] [DecidableEq α] [DecidableRel G.Adj] {n : ℕ} [Fintype β] [DecidableEq β] (f : α ↪ β) (hn : n ≠ 1) : SimpleGraph.cliqueFinset (SimpleGraph.map f G) n = Finset.map { toFun := Finset.map f, inj' := (_ : Function.Injective (Finset.map f)) } (SimpleGraph.cliqueFinset G n)

@[simp]

theorem SimpleGraph.cliqueFinset_map_of_equiv {α : Type u_1} {β : Type u_2} (G : SimpleGraph α) [Fintype α] [DecidableEq α] [DecidableRel G.Adj] [Fintype β] [DecidableEq β] (e : α ≃ β) (n : ℕ) : SimpleGraph.cliqueFinset (SimpleGraph.map (Equiv.toEmbedding e) G) n = Finset.map { toFun := Finset.map (Equiv.toEmbedding e), inj' := (_ : Function.Injective (Finset.map (Equiv.toEmbedding e))) } (SimpleGraph.cliqueFinset G n)