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.

Cliques

@[reducible, inline]

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

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

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

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

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

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

Equations

• G.instDecidableIsCliqueToSetOfDecidableEqOfDecidableRelAdj = decidable_of_iff' ((↑s).Pairwise G.Adj) ⋯

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

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

theorem SimpleGraph.IsClique.of_subsingleton {α : Type u_1} {s : Set α} {G : SimpleGraph α} (hs : s.Subsingleton) : G.IsClique s

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

@[simp]

theorem SimpleGraph.isClique_insert {α : Type u_1} {G : SimpleGraph α} {s : Set α} {a : α} : G.IsClique (insert a s) ↔ G.IsClique 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) : G.IsClique (insert a s) ↔ G.IsClique s ∧ ∀ b ∈ s, G.Adj a b

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

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

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

@[simp]

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

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

Alias of the forward direction of SimpleGraph.isClique_bot_iff.

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

theorem SimpleGraph.isClique_map_iff_of_nontrivial {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {f : α ↪ β} {t : Set β} (ht : t.Nontrivial) : (SimpleGraph.map f G).IsClique t ↔ ∃ (s : Set α), G.IsClique s ∧ ⇑f '' s = t

theorem SimpleGraph.isClique_map_iff {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {f : α ↪ β} {t : Set β} : (SimpleGraph.map f G).IsClique t ↔ t.Subsingleton ∨ ∃ (s : Set α), G.IsClique s ∧ ⇑f '' s = t

@[simp]

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

theorem SimpleGraph.isClique_map_finset_iff_of_nontrivial {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {f : α ↪ β} {t : Finset β} (ht : t.Nontrivial) : (SimpleGraph.map f G).IsClique ↑t ↔ ∃ (s : Finset α), G.IsClique ↑s ∧ Finset.map f s = t

theorem SimpleGraph.isClique_map_finset_iff {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {f : α ↪ β} {t : Finset β} : (SimpleGraph.map f G).IsClique ↑t ↔ t.card ≤ 1 ∨ ∃ (s : Finset α), G.IsClique ↑s ∧ Finset.map f s = t

theorem SimpleGraph.IsClique.finsetMap {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {f : α ↪ β} {s : Finset α} (h : G.IsClique ↑s) : (SimpleGraph.map f G).IsClique ↑(Finset.map f s)

theorem SimpleGraph.IsClique.of_induce {α : Type u_1} {G : SimpleGraph α} {S : G.Subgraph} {F : Set α} {A : Set ↑F} (c : (S.induce F).coe.IsClique A) : G.IsClique (Subtype.val '' A)

If a set of vertices A is a clique in subgraph of G induced by a superset of A, its embedding is a clique in G.

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.

• isClique : G.IsClique ↑s
• card_eq : s.card = n

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

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

Equations

• G.instDecidableIsNCliqueOfDecidableEqOfDecidableRelAdj = decidable_of_iff' (G.IsClique ↑s ∧ s.card = n) ⋯

@[simp]

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

@[simp]

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

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

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

theorem SimpleGraph.isNClique_map_iff {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {n : ℕ} (hn : 1 < n) {t : Finset β} {f : α ↪ β} : (SimpleGraph.map f G).IsNClique n t ↔ ∃ (s : Finset α), G.IsNClique n s ∧ Finset.map f s = t

@[simp]

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

@[simp]

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

@[simp]

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

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

theorem SimpleGraph.IsNClique.erase_of_mem {α : Type u_1} {G : SimpleGraph α} {n : ℕ} {s : Finset α} {a : α} [DecidableEq α] (hs : G.IsNClique n s) (ha : a ∈ s) : G.IsNClique (n - 1) (s.erase a)

theorem SimpleGraph.IsNClique.insert_erase {α : Type u_1} {G : SimpleGraph α} {n : ℕ} {s : Finset α} {a b : α} [DecidableEq α] (hs : G.IsNClique n s) (ha : ∀ w ∈ s \ {b}, G.Adj a w) (hb : b ∈ s) : G.IsNClique n (insert a (s.erase b))

theorem SimpleGraph.is3Clique_triple_iff {α : Type u_1} {G : SimpleGraph α} {a b c : α} [DecidableEq α] : G.IsNClique 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 α] : G.IsNClique 3 s ↔ ∃ (a : α) (b : α) (c : α), G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}

theorem SimpleGraph.is3Clique_iff_exists_cycle_length_three {α : Type u_1} {G : SimpleGraph α} : (∃ (s : Finset α), G.IsNClique 3 s) ↔ ∃ (u : α) (w : G.Walk u u), w.IsCycle ∧ w.length = 3

theorem SimpleGraph.IsNClique.of_induce {α : Type u_1} {G : SimpleGraph α} {S : G.Subgraph} {F : Set α} {s : Finset { x : α // x ∈ F }} {n : ℕ} (cc : (S.induce F).coe.IsNClique n s) : G.IsNClique n (Finset.map { toFun := Subtype.val, inj' := ⋯ } s)

If a set of vertices A is an n-clique in subgraph of G induced by a superset of A, its embedding is an n-clique in G.

Graphs without cliques

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

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

Equations

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

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

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

noncomputable def SimpleGraph.topEmbeddingOfNotCliqueFree {α : Type u_1} {G : SimpleGraph α} {n : ℕ} (h : ¬G.CliqueFree 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 : ℕ) : ¬G.CliqueFree n ↔ Nonempty (⊤ ↪g G)

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

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

@[simp]

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

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

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

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

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

@[simp]

theorem SimpleGraph.cliqueFree_map_iff {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {n : ℕ} {f : α ↪ β} [Nonempty α] : (SimpleGraph.map f G).CliqueFree n ↔ G.CliqueFree n

theorem SimpleGraph.cliqueFree_of_card_lt {α : Type u_1} {G : SimpleGraph α} {n : ℕ} [Fintype α] (hc : Fintype.card α < n) : G.CliqueFree 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) : (completeMultipartiteGraph V).CliqueFree 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 : G.CliqueFree n) (s t : α) : (G.replaceVertex s t).CliqueFree n

Clique-freeness is preserved by replaceVertex.

@[simp]

theorem SimpleGraph.cliqueFree_one {α : Type u_1} {G : SimpleGraph α} : G.CliqueFree 1 ↔ IsEmpty α

@[simp]

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

theorem SimpleGraph.CliqueFree.sup_edge {α : Type u_1} {G : SimpleGraph α} {n : ℕ} (h : G.CliqueFree n) (v w : α) : (G ⊔ edge v w).CliqueFree (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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

theorem SimpleGraph.CliqueFreeOn.of_succ {α : Type u_1} (G : SimpleGraph α) {s : Set α} {a : α} {n : ℕ} (hs : G.CliqueFreeOn s (n + 1)) (ha : a ∈ s) : G.CliqueFreeOn (s ∩ G.neighborSet 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

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

@[simp]

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

@[simp]

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

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

Alias of the reverse direction of SimpleGraph.cliqueSet_eq_empty_iff.

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

Clique number

noncomputable def SimpleGraph.cliqueNum {α : Type u_3} (G : SimpleGraph α) : ℕ

The maximum number of vertices in a clique of a graph G.

Equations

• G.cliqueNum = sSup {n : ℕ | ∃ (s : Finset α), G.IsNClique n s}

theorem SimpleGraph.IsClique.card_le_cliqueNum {α : Type u_3} {G : SimpleGraph α} [Fintype α] {t : Finset α} {tc : G.IsClique ↑t} : t.card ≤ G.cliqueNum

theorem SimpleGraph.exists_isNClique_cliqueNum {α : Type u_3} {G : SimpleGraph α} [Fintype α] : ∃ (s : Finset α), G.IsNClique G.cliqueNum s

structure SimpleGraph.IsMaximumClique {α : Type u_3} [Fintype α] (G : SimpleGraph α) (s : Finset α) : Prop

A maximum clique in a graph G is a clique with the largest possible size.

• isClique : G.IsClique ↑s
• maximum (t : Finset α) : G.IsClique ↑t → t.card ≤ s.card

theorem SimpleGraph.isMaximumClique_iff {α : Type u_3} {G : SimpleGraph α} [Fintype α] {s : Finset α} : G.IsMaximumClique s ↔ G.IsClique ↑s ∧ ∀ (t : Finset α), G.IsClique ↑t → t.card ≤ s.card

theorem SimpleGraph.isMaximalClique_iff {α : Type u_3} {G : SimpleGraph α} {s : Set α} : Maximal G.IsClique s ↔ G.IsClique s ∧ ∀ (t : Set α), G.IsClique t → s ⊆ t → t ⊆ s

A maximal clique in a graph G is a clique that cannot be extended by adding more vertices.

theorem SimpleGraph.IsMaximumClique.isMaximalClique {α : Type u_3} {G : SimpleGraph α} [Fintype α] (s : Finset α) (M : G.IsMaximumClique s) : Maximal G.IsClique ↑s

theorem SimpleGraph.maximumClique_card_eq_cliqueNum {α : Type u_3} {G : SimpleGraph α} [Fintype α] (s : Finset α) (sm : G.IsMaximumClique s) : s.card = G.cliqueNum

theorem SimpleGraph.maximumClique_exists {α : Type u_3} {G : SimpleGraph α} [Fintype α] : ∃ (s : Finset α), G.IsMaximumClique s

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

• G.cliqueFinset n = Finset.filter (fun (s : Finset α) => G.IsNClique n s) Finset.univ

@[simp]

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

@[simp]

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

@[simp]

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

theorem SimpleGraph.CliqueFree.cliqueFinset {α : Type u_1} {G : SimpleGraph α} [Fintype α] [DecidableEq α] [DecidableRel G.Adj] {n : ℕ} : G.CliqueFree n → G.cliqueFinset 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 : ℕ} : (G.cliqueFinset n).card ≤ (Fintype.card α).choose n

theorem SimpleGraph.cliqueFinset_mono {α : Type u_1} {G : SimpleGraph α} (H : SimpleGraph α) [Fintype α] [DecidableEq α] [DecidableRel G.Adj] {n : ℕ} [DecidableRel H.Adj] (h : G ≤ H) : G.cliqueFinset n ⊆ H.cliqueFinset 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.map f G).cliqueFinset n = Finset.map { toFun := Finset.map f, inj' := ⋯ } (G.cliqueFinset 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.map e.toEmbedding G).cliqueFinset n = Finset.map { toFun := Finset.map e.toEmbedding, inj' := ⋯ } (G.cliqueFinset n)

Independent Sets

@[reducible, inline]

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

An independent set in a graph is a set of vertices that are pairwise not adjacent.

Equations

• G.IsIndepSet s = s.Pairwise fun (v w : α) => ¬G.Adj v w

theorem SimpleGraph.isIndepSet_iff {α : Type u_1} (G : SimpleGraph α) {s : Set α} : G.IsIndepSet s ↔ s.Pairwise fun (v w : α) => ¬G.Adj v w

@[simp]

theorem SimpleGraph.isClique_compl {α : Type u_1} (G : SimpleGraph α) {s : Set α} : Gᶜ.IsClique s ↔ G.IsIndepSet s

An independent set is a clique in the complement graph and vice versa.

@[simp]

theorem SimpleGraph.isIndepSet_compl {α : Type u_1} (G : SimpleGraph α) {s : Set α} : Gᶜ.IsIndepSet s ↔ G.IsClique s

An independent set in the complement graph is a clique and vice versa.

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

Equations

• G.instDecidableIsIndepSetToSetOfDecidableEqOfDecidableRelAdj = decidable_of_iff' ((↑s).Pairwise fun (v w : α) => ¬G.Adj v w) ⋯

theorem SimpleGraph.IsIndepSet.nonempty_mem_compl_mem_edge {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableEq α] {s : Finset α} (indA : G.IsIndepSet ↑s) {e : Sym2 α} (he : e ∈ G.edgeSet) : (Finset.filter (fun (b : α) => b ∈ e) sᶜ).Nonempty

If s is an independent set, its complement meets every edge of G.

theorem SimpleGraph.isIndepSet_neighborSet_of_triangleFree {α : Type u_1} (G : SimpleGraph α) [DecidableEq α] (h : G.CliqueFree 3) (v : α) : G.IsIndepSet (G.neighborSet v)

The neighbors of a vertex v form an independent set in a triangle free graph G.

theorem SimpleGraph.isIndepSet_induce {α : Type u_1} (G : SimpleGraph α) {F : Set α} {s : Set ↑F} : (⊤.induce F).coe.IsIndepSet s ↔ G.IsIndepSet (Subtype.val '' s)

The embedding of an independent set of an induced subgraph of the subgraph G is an independent set in G and vice versa.

N-Independent sets

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

An n-independent set in a graph is a set of n vertices which are pairwise nonadjacent.

• isIndepSet : G.IsIndepSet ↑s
• card_eq : s.card = n

theorem SimpleGraph.isNIndepSet_iff {α : Type u_1} (G : SimpleGraph α) (n : ℕ) (s : Finset α) : G.IsNIndepSet n s ↔ G.IsIndepSet ↑s ∧ s.card = n

@[simp]

theorem SimpleGraph.isNClique_compl {α : Type u_1} (G : SimpleGraph α) {n : ℕ} {s : Finset α} : Gᶜ.IsNClique n s ↔ G.IsNIndepSet n s

An n-independent set is an n-clique in the complement graph and vice versa.

@[simp]

theorem SimpleGraph.isNIndepSet_compl {α : Type u_1} (G : SimpleGraph α) {n : ℕ} {s : Finset α} : Gᶜ.IsNIndepSet n s ↔ G.IsNClique n s

An n-independent set in the complement graph is an n-clique and vice versa.

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

Equations

• G.instDecidableIsNIndepSetOfDecidableEqOfDecidableRelAdj = decidable_of_iff' (G.IsIndepSet ↑s ∧ s.card = n) ⋯

theorem SimpleGraph.isNIndepSet_induce {α : Type u_1} (G : SimpleGraph α) {F : Set α} {s : Finset { x : α // x ∈ F }} {n : ℕ} : (⊤.induce F).coe.IsNIndepSet n s ↔ G.IsNIndepSet n (Finset.map { toFun := Subtype.val, inj' := ⋯ } s)

The embedding of an n-independent set of an induced subgraph of the subgraph G is an n-independent set in G and vice versa.

Graphs without independent sets

def SimpleGraph.IndepSetFree {α : Type u_1} (G : SimpleGraph α) (n : ℕ) : Prop

G.IndepSetFree n means that G has no n-independent sets.

Equations

• G.IndepSetFree n = ∀ (t : Finset α), ¬G.IsNIndepSet n t

@[simp]

theorem SimpleGraph.cliqueFree_compl {α : Type u_1} (G : SimpleGraph α) {n : ℕ} : Gᶜ.CliqueFree n ↔ G.IndepSetFree n

An graph is n-independent set free iff its complement is n-clique free.

@[simp]

theorem SimpleGraph.indepSetFree_compl {α : Type u_1} (G : SimpleGraph α) {n : ℕ} : Gᶜ.IndepSetFree n ↔ G.CliqueFree n

An graph's complement is n-independent set free iff it is n-clique free.

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

G.IndepSetFreeOn s n means that G has no n-independent sets contained in s.

Equations

• G.IndepSetFreeOn s n = ∀ ⦃t : Finset α⦄, ↑t ⊆ s → ¬G.IsNIndepSet n t

Set of independent sets

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

The n-independent sets in a graph as a set.

Equations

• G.indepSetSet n = {s : Finset α | G.IsNIndepSet n s}

@[simp]

theorem SimpleGraph.mem_indepSetSet_iff {α : Type u_1} {G : SimpleGraph α} {n : ℕ} {s : Finset α} : s ∈ G.indepSetSet n ↔ G.IsNIndepSet n s

Independence Number

noncomputable def SimpleGraph.indepNum {α : Type u_3} (G : SimpleGraph α) : ℕ

The maximal number of vertices of an independent set in a graph G.

Equations

• G.indepNum = sSup {n : ℕ | ∃ (s : Finset α), G.IsNIndepSet n s}

@[simp]

theorem SimpleGraph.cliqueNum_compl {α : Type u_3} {G : SimpleGraph α} : Gᶜ.cliqueNum = G.indepNum

@[simp]

theorem SimpleGraph.indepNum_compl {α : Type u_3} {G : SimpleGraph α} : Gᶜ.indepNum = G.cliqueNum

theorem SimpleGraph.IsIndepSet.card_le_indepNum {α : Type u_3} {G : SimpleGraph α} [Fintype α] {t : Finset α} (tc : G.IsIndepSet ↑t) : t.card ≤ G.indepNum

theorem SimpleGraph.exists_isNIndepSet_indepNum {α : Type u_3} {G : SimpleGraph α} [Fintype α] : ∃ (s : Finset α), G.IsNIndepSet G.indepNum s

structure SimpleGraph.IsMaximumIndepSet {α : Type u_3} [Fintype α] (G : SimpleGraph α) (s : Finset α) : Prop

An independent set in a graph G such that there is no independent set with more vertices.

• isIndepSet : G.IsIndepSet ↑s
• maximum (t : Finset α) : G.IsIndepSet ↑t → t.card ≤ s.card

theorem SimpleGraph.isMaximumIndepSet_iff {α : Type u_3} [Fintype α] (G : SimpleGraph α) (s : Finset α) : G.IsMaximumIndepSet s ↔ G.IsIndepSet ↑s ∧ ∀ (t : Finset α), G.IsIndepSet ↑t → t.card ≤ s.card

@[simp]

theorem SimpleGraph.isMaximumClique_compl {α : Type u_3} {G : SimpleGraph α} [Fintype α] (s : Finset α) : Gᶜ.IsMaximumClique s ↔ G.IsMaximumIndepSet s

@[simp]

theorem SimpleGraph.isMaximumIndepSet_compl {α : Type u_3} {G : SimpleGraph α} [Fintype α] (s : Finset α) : Gᶜ.IsMaximumIndepSet s ↔ G.IsMaximumClique s

theorem SimpleGraph.isMaximalIndepSet_iff {α : Type u_3} {G : SimpleGraph α} {s : Set α} : Maximal G.IsIndepSet s ↔ G.IsIndepSet s ∧ ∀ (t : Set α), G.IsIndepSet t → s ⊆ t → t ⊆ s

An independent set in a graph G that cannot be extended by adding more vertices.

@[simp]

theorem SimpleGraph.isMaximalClique_compl {α : Type u_3} {G : SimpleGraph α} (s : Finset α) : Maximal Gᶜ.IsClique ↑s ↔ Maximal G.IsIndepSet ↑s

@[simp]

theorem SimpleGraph.isMaximalIndepSet_compl {α : Type u_3} {G : SimpleGraph α} (s : Finset α) : Maximal Gᶜ.IsIndepSet ↑s ↔ Maximal G.IsClique ↑s

theorem SimpleGraph.IsMaximumIndepSet.isMaximalIndepSet {α : Type u_3} {G : SimpleGraph α} [Fintype α] (s : Finset α) (M : G.IsMaximumIndepSet s) : Maximal G.IsIndepSet ↑s

theorem SimpleGraph.maximumIndepSet_card_eq_indepNum {α : Type u_3} {G : SimpleGraph α} [Fintype α] (t : Finset α) (tmc : G.IsMaximumIndepSet t) : t.card = G.indepNum

theorem SimpleGraph.maximumIndepSet_exists {α : Type u_3} {G : SimpleGraph α} [Fintype α] : ∃ (s : Finset α), G.IsMaximumIndepSet s

Finset of independent sets

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

The n-independent sets in a graph as a finset.

Equations

• G.indepSetFinset n = Finset.filter (fun (s : Finset α) => G.IsNIndepSet n s) Finset.univ

@[simp]

theorem SimpleGraph.mem_indepSetFinset_iff {α : Type u_1} {G : SimpleGraph α} [Fintype α] [DecidableEq α] [DecidableRel G.Adj] {n : ℕ} {s : Finset α} : s ∈ G.indepSetFinset n ↔ G.IsNIndepSet n s