Mathlib Map

Theorems · Definition · combinatorics

SimpleGraph.cliqueSet

{α : Type u_1} → SimpleGraph α → ℕ → Set (Finset α)

The n-cliques in a graph as a set.

Defined in
Mathlib.Combinatorics.SimpleGraph.Clique
Cited by
18 results in Mathlib
Foundations
Depth 2 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

SimpleGraph.EdgeDisjointTriangles · cited by 8SimpleGraph.EdgeDisjointT…SimpleGraph.coe_cliqueFinset · cited by 5SimpleGraph.coe_cliqueFin…SimpleGraph.cliqueSet_map · cited by 3SimpleGraph.cliqueSet_mapSimpleGraph.cliqueSet_mono · cited by 2SimpleGraph.cliqueSet_monoSimpleGraph.TripartiteFromTriangles.cliqueSet_eq_image · cited by 2TripartiteFromTriangles.c…SimpleGraph.cliqueSet_bot · cited by 1SimpleGraph.cliqueSet_botSimpleGraph.cliqueSet_eq_empty_iff · cited by 1SimpleGraph.cliqueSet_eq_…SimpleGraph.cliqueSet_map_of_equiv · cited by 1SimpleGraph.cliqueSet_map…SimpleGraph.cliqueSet_one · cited by 1SimpleGraph.cliqueSet_oneSimpleGraph.edgeDisjointTriangles_iff_mem_sym2_subsingleton · cited by 1SimpleGraph.edgeDisjointT…SimpleGraph.EdgeDisjointTriangles.map · cited by 1EdgeDisjointTriangles.mapSimpleGraph.EdgeDisjointTriangles.mem_sym2_subsingleton · cited by 1EdgeDisjointTriangles.mem…SimpleGraph.cliqueFinset_map · cited by 1SimpleGraph.cliqueFinset_…SimpleGraph.CliqueFree.cliqueSet · cited by 1CliqueFree.cliqueSetSimpleGraph.TripartiteFromTriangles.toTriangle_surjOn · cited by 0TripartiteFromTriangles.t…Set · cited by 53352SetFinset · cited by 13712FinsetSet.ofPred · cited by 6101Set.ofPredSimpleGraph · cited by 3072SimpleGraphSimpleGraph.IsNClique · cited by 64SimpleGraph.IsNCliqueSimpleGraph.cliqueSetCITED BYCITES

Cites5

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by19

Results whose statement or proof uses this declaration.