Erdős problem 760

The cochromatic number of $G$ , denoted by $\zeta(G)$ , is the minimum number of colours needed to colour the vertices of $G$ such that each colour class induces either a complete graph or independent set.

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

760.lean

Retained formal statement2 of 2

A problem of Erdős and Gimbel, who proved that there must exist a subgraph $H$ with $\zeta(H) \gg \left(\frac{m}{\log m}\right)^{1/2}.$

FormalConjectures/ErdosProblems/760.leanErdos760.erdos_760.variants.erdos_gimbel3 linesExact file

1∃ c > 0,2  ∀ (V : Type u_1) [Finite V] (G : SimpleGraph V) (m : ℕ),3    G.chromaticNumber = ↑m → ∃ H k, ↑k ≤ H.coe.cochromaticNumber ∧ c * √(↑m / Real.log ↑m) ≤ ↑k

SolvedStatement only, no proof