A clique is a set of pairwise adjacent vertices and an independent set a set of pairwise non-adjacent vertices, both in mathlib's $Set$-valued, $Prop$-valued form ($IsIndepSet$ is by definition pairwise non-adjacency, so no complement graph and no decidability appear in the statement). Sizes are counted with $Set.ncard$ and stated as "at least", as everywhere in this submission.

Graphs range over the canonical carriers $Fin n$ for all $n$ beyond the bound, so the statement applies to a graph on any finite vertex set by transport along a bijection.

This is the two-colour case of the multicolour concept of this submission — colour a pair by whether it is an edge — and it is proved that way, by a glue proof assuming that statement. It gets its own statement because it is the form the literature cites and the form graph-theoretic applications consume, and because a submission's headline should not be reachable only through a strengthening.