Defining independent sets directly or through complement

Stream: mathlib4

[Christoph Spiegel]

Given that cliques are already established in mathlib and independent sets are not, would it be more appropriate to define independent sets from scratch a la s.Pairwise (fun v w ↦ ¬G.Adj v w) and then establish the relation to cliques in the complement through a set of lemmas or should the base definition already work with the complement, i.e., Gᶜ.IsClique s? My gut feeling is that the former is the better way, since this allows people to just work with independent sets directly if that's what the statement is about without switching to the complement (and having an additional rw step). It's also how one would define it in graph theory course. @Kyle Miller @Yaël Dillies @Bhavik Mehta

[Yaël Dillies]

Bhavik has some independent set API somewhere. We should move it to mathlib

[Christoph Spiegel]

Great, should have asked before getting started :big_smile:

[Christoph Spiegel]

@Bhavik Mehta can you point us to the code and then we can try to PR that?