Theorems · Definition · combinatorics
SimpleGraph.cliqueFinset
{α : Type u_1} → (G : SimpleGraph α) → [Fintype α] → [DecidableEq α] → [DecidableRel G.Adj] → ℕ → Finset (Finset α)The n-cliques in a graph as a finset.
- Defined in
- Mathlib.Combinatorics.SimpleGraph.Clique
- Cited by
- 26 results in Mathlib
- Foundations
- Depth 67 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetstatement and proof · cited by 13,712
- Fintypestatement and proof · cited by 7,736
- Finset.univproof · cited by 3,473
- SimpleGraphstatement and proof · cited by 3,072
- SimpleGraph.Adjstatement and proof · cited by 1,346
- Finset.filterproof · cited by 949
- SimpleGraph.IsNCliqueproof · cited by 64
Cited by27
Results whose statement or proof uses this declaration.
- ruzsaSzemerediNumberproof · cited by 8
- SimpleGraph.coe_cliqueFinsetstatement · cited by 5
- SimpleGraph.cliqueFinset_eq_empty_iffstatement · cited by 3
- SimpleGraph.TripartiteFromTriangles.card_trianglesstatement · cited by 2
- SimpleGraph.farFromTriangleFree_of_disjoint_trianglesstatement and proof · cited by 2
- ruzsaSzemerediNumber_monoproof · cited by 2
- SimpleGraph.FarFromTriangleFree.le_card_cliqueFinsetstatement and proof · cited by 2
- corners_theoremproof · cited by 2
- SimpleGraph.mem_cliqueFinset_iffstatement · cited by 1
- SimpleGraph.EdgeDisjointTriangles.card_edgeFinset_lestatement and proof · cited by 1
- SimpleGraph.card_cliqueFinset_lestatement and proof · cited by 1
- SimpleGraph.TripartiteFromTriangles.cliqueFinset_eq_imagestatement and proof · cited by 1