TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-03

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The bounds $\omega(G)\leq\chi(G)$ and $|V(G)|\leq\chi(G)\alpha(G)$

Statement

For every finite simple graph $G=(V,E)$ ,

$\omega(G)\leq\chi(G),\qquad |V|\leq\chi(G)\alpha(G).$

Both inequalities include the null graph, where all displayed quantities are $0$ .

Facts & Assumptions

Given: A finite simple graph $G=(V,E)$ and a proper $\chi(G)$ -colouring $c:V\to\chi(G)$ .

[L1]

Adjacent vertices receive different colours, and the fibres $C_j:=c^{-1}[\{j\}]$ are the colour classes (Proper vertex colourings and chromatic number).

[L2]

A clique has all pairs adjacent, an independent set has no adjacent pair, and $\omega(G)$ and $\alpha(G)$ are the corresponding maximum cardinalities (Cliques, independent sets, clique number and independence number).

[L3]

The cardinality of a finite disjoint union is the sum of the cardinalities of its blocks (The sum rule: a finite disjoint union is finite with $\lvert A \cup B\rvert = \lvert A\rvert + \lvert B\rvert$ and $\lvert\bigcup_{i \in I} A_i\rvert = \sum_{i \in I}\lvert A_i\rvert$ , and a sum over a finite index set splits along a partition, clause 2).

Proof

technique · direct

1.1

If $K$ is a clique, then [L1] makes $c|_K$ injective into the $\chi(G)$ -element colour set, so $|K|\leq\chi(G)$ ; maximizing over cliques gives $\omega(G)\leq\chi(G)$ .

L1L2

1.2

Each colour class $C_j$ is independent, since two vertices in it have the same colour and therefore cannot be adjacent by [L1]; hence $|C_j|\leq\alpha(G)$ by [L2].

L1L2

2.1

The colour classes are pairwise disjoint and have union $V$ , so [L3] and step 1.2 give $|V|=\sum_{j\in\chi(G)}|C_j|\leq\sum_{j\in\chi(G)}\alpha(G)=\chi(G)\alpha(G)$ .

step 1.2L3

3.1

Steps 1.1 and 2.1 prove the two claimed bounds, including the empty family of colour classes when $V=\varnothing$ .

step 1.1step 2.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 64 results over 21 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

Bondy and Murty, Graph Theory, Stable Sets and Cliques (standard reference, not scraped)

The bounds ω(G)≤χ(G)\omega(G)\leq\chi(G)ω(G)≤χ(G) and ∣V(G)∣≤χ(G)α(G)|V(G)|\leq\chi(G)\alpha(G)∣V(G)∣≤χ(G)α(G)