Theorems · Definition · combinatorics
SimpleGraph.IsClique
{α : Type u_1} → SimpleGraph α → Set α → PropA clique in a graph is a set of vertices that are pairwise adjacent.
- Defined in
- Mathlib.Combinatorics.SimpleGraph.Clique
- Cited by
- 76 results in Mathlib
- Foundations
- Depth 5 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- SimpleGraphstatement and proof · cited by 3,072
- SimpleGraph.Adjproof · cited by 1,346
- Set.Pairwiseproof · cited by 321
Cited by80
Results whose statement or proof uses this declaration.
- SimpleGraph.IsNClique.isCliquestatement · cited by 14
- SimpleGraph.isNClique_iffstatement and proof · cited by 5
- SimpleGraph.IsClique.card_le_cliqueNumstatement and proof · cited by 4
- SimpleGraph.IsClique.subsetstatement · cited by 4
- SimpleGraph.IsNClique.insertproof · cited by 3
- SimpleGraph.cliqueSet_mapproof · cited by 3
- SimpleGraph.IsClique.mapstatement and proof · cited by 3
- SimpleGraph.IsClique.sdiff_of_sup_edgestatement and proof · cited by 3
- SimpleGraph.isClique_iffstatement · cited by 3
- SimpleGraph.IsNClique.casesOnstatement and proof · cited by 2
- SimpleGraph.IsNClique.mapproof · cited by 2
- SimpleGraph.IsClique.card_le_of_colorablestatement and proof · cited by 2