Graph cliques #
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 an
-clique.simple_graph.clique_finset
: Finset ofn
-cliques of a graph.simple_graph.clique_free
: Predicate for a graph to have non
-cliques.
TODO #
- Clique numbers
- Going back and forth between cliques and complete subgraphs or embeddings of complete graphs.
- Do we need
clique_set
, a version ofclique_finset
for infinite graphs?
Cliques #
A clique in a graph is a set of vertices that are pairwise adjacent.
@[protected, instance]
def
simple_graph.is_clique.decidable
{α : Type u_1}
(G : simple_graph α)
[decidable_eq α]
[decidable_rel G.adj]
{s : finset α} :
Equations
theorem
simple_graph.is_clique.subset
{α : Type u_1}
{G : simple_graph α}
{s t : set α}
(h : t ⊆ s) :
@[simp]
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 #
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
@[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
- simple_graph.is_n_clique.decidable G = decidable_of_iff' (G.is_clique ↑s ∧ s.card = n) _
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
theorem
simple_graph.is_3_clique_triple_iff
{α : Type u_1}
{G : simple_graph α}
[decidable_eq α]
{a b c : α} :
theorem
simple_graph.is_3_clique_iff
{α : Type u_1}
{G : simple_graph α}
{s : finset α}
[decidable_eq α] :
Graphs without cliques #
G.clique_free n
means that G
has no n
-cliques.
Equations
- G.clique_free n = ∀ (t : finset α), ¬G.is_n_clique n t
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
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 #
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
- G.clique_finset n = finset.filter (G.is_n_clique n) finset.univ
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
@[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
@[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`.
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