Greedy colorings along a well-founded order #
If every edge joins comparable vertices of a well-founded relation and every vertex has
finitely many neighbours below it, coloring each vertex by the least natural number not
used by its neighbours below is a proper coloring by ℕ.
theorem
Erdos111.nonempty_coloring_of_wellFounded
{V : Type u_1}
(H : SimpleGraph V)
{r : V → V → Prop}
(hr : WellFounded r)
(hcomp : ∀ (u v : V), H.Adj u v → r u v ∨ r v u)
(hfin : ∀ (v : V), {u : V | r u v ∧ H.Adj u v}.Finite)
:
Greedy coloring along a well-founded relation with finitely many earlier neighbours.