Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-09 23:54 b7f7c4aa

View on Github →

feat(combinatorics/simple_graph/clique): Cliques (#12982) Define cliques.

Estimated changes

Created src/combinatorics/simple_graph/clique.lean

added theorem simple_graph.is_clique.mono

added theorem simple_graph.is_clique.subset

added structure simple_graph.is_clique

added theorem simple_graph.is_clique_iff

added theorem simple_graph.is_n_clique.mono

added structure simple_graph.is_n_clique

added theorem simple_graph.is_n_clique_iff

Modified src/data/finset/pairwise.lean