Graph cliques #
This file defines cliques in simple graphs. A clique is a set of vertices that are pairwise
Main declarations #
- Clique numbers
- Going back and forth between cliques and complete subgraphs or embeddings of complete graphs.
- Do we need
clique_set, a version of
clique_finset for infinite graphs?
A clique in a graph is a set of vertices that are pairwise adjacent.
Alias of the forward direction of simple_graph.is_clique_bot_iff`.
n-clique in a graph is a set of
n vertices which are pairwise connected.
G.clique_free n means that
G has no
n-cliques in a graph as a finset.
Alias of the reverse direction of simple_graph.clique_finset_eq_empty_iff`.