Erdős problem 760
The cochromatic number of , denoted by , is the minimum number of colours needed to colour the vertices of such that each colour class induces either a complete graph or independent set.
Sources
FormalConjectures/ErdosProblems/
760.lean
The cochromatic number of , denoted by , is the minimum number of colours needed to colour the vertices of such that each colour class induces either a complete graph or independent set.
If is a graph with chromatic number then must contain a subgraph with
A problem of Erdős and Gimbel, who proved that there must exist a subgraph with The proposed bound would be best possible, as shown by taking to be a complete graph.
The answer is yes, proved by Alon, Krivelevich, and Sudakov.
True ↔ ∃ c > 0, ∀ (V : Type u_1) [Finite V] (G : SimpleGraph V) (m : ℕ), G.chromaticNumber = ↑m → ∃ H k, ↑k ≤ H.coe.cochromaticNumber ∧ c * ↑m / Real.log ↑m ≤ ↑k