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 ann
-clique.SimpleGraph.cliqueFinset
: Finset ofn
-cliques of a graph.SimpleGraph.CliqueFree
: Predicate for a graph to have non
-cliques.
TODO #
- Clique numbers
- Do we need
cliqueSet
, a version ofcliqueFinset
for infinite graphs?
Cliques #
A clique in a graph is a set of vertices that are pairwise adjacent.
Instances For
A clique is a set of vertices whose induced graph is complete.
Alias of the forward direction of SimpleGraph.isClique_bot_iff
.
n
-cliques #
- clique : SimpleGraph.IsClique G ↑s✝
- card_eq : Finset.card s✝ = n
An n
-clique in a graph is a set of n
vertices which are pairwise connected.
Instances For
Graphs without cliques #
G.CliqueFree n
means that G
has no n
-cliques.
Instances For
An embedding of a complete graph that witnesses the fact that the graph is not clique-free.
Instances For
See SimpleGraph.cliqueFree_of_chromaticNumber_lt
for a tighter bound.
A complete r
-partite graph has no n
-cliques for r < n
.
Set of cliques #
The n
-cliques in a graph as a set.
Instances For
Alias of the reverse direction of SimpleGraph.cliqueSet_eq_empty_iff
.
Finset of cliques #
The n
-cliques in a graph as a finset.
Instances For
Alias of the reverse direction of SimpleGraph.cliqueFinset_eq_empty_iff
.