[Merged by Bors] - feat(combinatorics/simple_graph): More clique lemmas

[YaelDillies]

More lemmas about is_clique, is_n_clique, edge_set. Also define clique_free_on, a local version of clique_free.

---

clique_free_on is to be used in John Talbot's formalisation of Turán's theorem.

[bors[bot]]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here. For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build mathlib
• Lint mathlib
• Lint style
• Run tests