Erdős problem 914

Let $r\geq 2$ and $m\geq 1$ . Every graph with $rm$ vertices and minimum degree at least $m(r-1)$ contains $m$ vertex disjoint copies of $K_r$ .

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

914.lean

Retained formal statement2 of 2

Equivalently, every graph with $rm$ vertices and maximum degree at most $m-1$ has a proper vertex colouring with $m$ colours in which every colour class has exactly $r$ vertices (an equitable colouring).

FormalConjectures/ErdosProblems/914.leanErdos914.erdos_914.variants.equitable_colouring5 linesExact file

1∀ {r m : ℕ},2  2 ≤ r →3    1 ≤ m →4      ∀ {V : Type u_1} [inst : Fintype V] (G : SimpleGraph V) [inst_1 : DecidableRel G.Adj],5        Fintype.card V = r * m → G.maxDegree ≤ m - 1 → ∃ C, ∀ (i : Fin m), (C.colorClass i).ncard = r

SolvedStatement only, no proof