Ported to Lean Pool from jtraverso/hajnal-szemeredi, commit
ba34061e3cf12dfc8297610d5d7b3f0afac7ec54; import paths adapted.
Lema 2.1 de Kierstead–Kostochka #
Si la clase grande hi de una coloración casi equitativa es accesible (alcanza a la clase
pequeña lo en el digrafo auxiliar H), moviendo un vértice a lo largo de un camino de hi a
lo se obtiene una coloración equitativa.
Para evitar caminos simples, inducimos sobre un conjunto K de clases permitidas: tras mover un
vértice de hi a la siguiente clase j, el resto del camino evita hi, y basta con K \ {hi}.
theorem
HajnalSzemeredi.mem_palette_of_reach
{V : Type u_1}
{G : SimpleGraph V}
{S : Finset V}
{P : Finset ℕ}
{c : V → ℕ}
(hc : Into S c P)
{R : ℕ → ℕ → Prop}
(hR : ∀ (a b : ℕ), R a b → Mov G S c a b)
{j lo : ℕ}
(h : Relation.ReflTransGen R j lo)
(hj : j ≠ lo)
:
Si j ≠ lo alcanza a lo, la clase j es no vacía y por tanto está en la paleta.
theorem
HajnalSzemeredi.shift_of_acc
{V : Type u_1}
{G : SimpleGraph V}
{S : Finset V}
{P : Finset ℕ}
{c : V → ℕ}
{s lo hi : ℕ}
(hc : IsNear G S P c s lo hi)
(hacc : Relation.ReflTransGen (Mov G S c) hi lo)
:
Lema 2.1. Si la clase grande es accesible, hay una coloración equitativa.