Commit 2026-01-29 20:08 62a82d6d

feat(Combinatorics): a clique has size at most the chromatic number (#32654) There already exists a version of this lemma for cliques given by a set, but it's impractical to provide an explicit clique on an explicit graph as a set, rather than an indexed family, especially because computing the size of the set would then involve proving that it is the range of an injective function, even though being a clique already implies being injective! Application: google-deepmind/formal-conjectures#1369 Also rename coloringOfIsEmpty and colorable_of_isEmpty to leverage anonymous dot notation, and make more arguments implicit. From FormalConjectures