Ported to Lean Pool from jtraverso/hajnal-szemeredi, commit ba34061e3cf12dfc8297610d5d7b3f0afac7ec54; import paths adapted.

Definitions for the equitable-colouring counting argument

Abstraemos la situación del artículo en CountHyp:

• PA (clases accesibles) y PB (inaccesibles) son paletas disjuntas que cubren los colores de S; A, B son los vértices con color en PA, PB;
• TU ⊆ PA es la familia 𝒜', con t = |TU| clases, todas de tamaño s;
• q = |PB|, |B| = q s + 1, grado máximo r con r + 1 = |PA| + |PB|;
• (2.1): todo y ∈ B tiene un vecino en cada clase de PA;
• (2.2): todo x con color en TU tiene al menos |PA| - 1 - t vecinos en A.

Una arista zy (z con color W ∈ TU, y ∈ B) es solo si z es el único vecino de y en la clase W. Sz z son los vecinos especiales de z (en B) y Sy y los de y (en A').

def HajnalSzemeredi.part {V : Type u_1} (S : Finset V) (c : V → ℕ) (Q : Finset ℕ) : Finset V

Vértices de S con color en la paleta Q.

Equations

• HajnalSzemeredi.part S c Q = {v ∈ S | c v ∈ Q}

noncomputable def HajnalSzemeredi.nIn {V : Type u_1} (G : SimpleGraph V) (S : Finset V) (c : V → ℕ) (y : V) (W : ℕ) : Finset V

Vecinos de y en la clase W.

Equations

• HajnalSzemeredi.nIn G S c y W = HajnalSzemeredi.nbr G S y ∩ HajnalSzemeredi.cls S c W

def HajnalSzemeredi.IsSolo {V : Type u_1} (G : SimpleGraph V) (S : Finset V) (c : V → ℕ) (TU : Finset ℕ) (B : Finset V) (z y : V) : Prop

zy es una arista solo (respecto a la familia TU y al conjunto B).

Equations

• HajnalSzemeredi.IsSolo G S c TU B z y = (z ∈ S ∧ c z ∈ TU ∧ y ∈ B ∧ HajnalSzemeredi.nIn G S c y (c z) = {z})

noncomputable def HajnalSzemeredi.Sz {V : Type u_1} (G : SimpleGraph V) (S : Finset V) (c : V → ℕ) (TU : Finset ℕ) (B : Finset V) (z : V) : Finset V

Vecinos especiales de z.

Equations

• HajnalSzemeredi.Sz G S c TU B z = {y ∈ B | HajnalSzemeredi.IsSolo G S c TU B z y}

noncomputable def HajnalSzemeredi.Sy {V : Type u_1} (G : SimpleGraph V) (S : Finset V) (c : V → ℕ) (TU : Finset ℕ) (B : Finset V) (y : V) : Finset V

Vecinos especiales de y.

Equations

• HajnalSzemeredi.Sy G S c TU B y = {z ∈ S | HajnalSzemeredi.IsSolo G S c TU B z y}

structure HajnalSzemeredi.CountHyp {V : Type u_1} (G : SimpleGraph V) (S : Finset V) (c : V → ℕ) (PA PB TU : Finset ℕ) (r s : ℕ) : Prop

Hipótesis de la parte de conteo.

• disj : Disjoint PA PB
• cover (v : V) : v ∈ S → c v ∈ PA ∪ PB
• sub : TU ⊆ PA
• ne : TU.Nonempty
• card_r : r + 1 = PA.card + PB.card
• deg : DegLe G S r
• size (W : ℕ) : W ∈ TU → (cls S c W).card = s
• card_B : (part S c PB).card = PB.card * s + 1
• h21 (y : V) : y ∈ part S c PB → ∀ X ∈ PA, (nIn G S c y X).Nonempty

  (2.1)

• h22 (x : V) : x ∈ S → c x ∈ TU → PA.card ≤ (nbr G (part S c PA) x).card + TU.card + 1

  (2.2)