Graph cliques #
This file defines cliques in simple graphs. A clique is a set of vertices that are pairwise
Main declarations #
- Clique numbers
- 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.
A clique is a set of vertices whose induced graph is complete.
n-clique in a graph is a set of
n vertices which are pairwise connected.
G.clique_free n means that
G has no
An embedding of a complete graph that witnesses the fact that the graph is not clique-free.
simple_graph.clique_free_chromatic_number_succ for a tighter bound.
n-cliques in a graph as a set.
n-cliques in a graph as a finset.