Finite colour classes and proper edge colourings

Colour classes partition a finite set. For graph edges, properness means that two distinct edges of the same colour have disjoint endpoints.

def LeanPool.Vizing.ColourClasses.colourClass {α : Type u_1} {β : Type u_2} [DecidableEq β] (S : Finset α) (colour : α → β) (b : β) : Finset α

The elements of S assigned the literal colour b.

Equations

• LeanPool.Vizing.ColourClasses.colourClass S colour b = {a ∈ S | colour a = b}

def LeanPool.Vizing.ColourClasses.usedColours {α : Type u_1} {β : Type u_2} [DecidableEq β] (S : Finset α) (colour : α → β) : Finset β

The palette actually used by a finite coloured set.

Equations

• LeanPool.Vizing.ColourClasses.usedColours S colour = Finset.image colour S

theorem LeanPool.Vizing.ColourClasses.mem_colourClass {α : Type u_1} {β : Type u_2} [DecidableEq β] {S : Finset α} {colour : α → β} {b : β} {a : α} : a ∈ colourClass S colour b ↔ a ∈ S ∧ colour a = b

theorem LeanPool.Vizing.ColourClasses.colourClass_subset {α : Type u_1} {β : Type u_2} [DecidableEq β] (S : Finset α) (colour : α → β) (b : β) : colourClass S colour b ⊆ S

theorem LeanPool.Vizing.ColourClasses.disjoint_colourClass {α : Type u_1} {β : Type u_2} [DecidableEq β] {S : Finset α} {colour : α → β} {b d : β} (hbd : b ≠ d) : Disjoint (colourClass S colour b) (colourClass S colour d)

theorem LeanPool.Vizing.ColourClasses.biUnion_colourClass {α : Type u_1} {β : Type u_2} [DecidableEq β] [DecidableEq α] (S : Finset α) (colour : α → β) : (usedColours S colour).biUnion (colourClass S colour) = S

theorem LeanPool.Vizing.ColourClasses.card_eq_sum_card_colourClass {α : Type u_1} {β : Type u_2} [DecidableEq β] (S : Finset α) (colour : α → β) : S.card = ∑ b ∈ usedColours S colour, (colourClass S colour b).card

Exact cardinal ledger for the colour classes.

Proper edge colours

def LeanPool.Vizing.ColourClasses.ProperOn {β : Type u_2} {V : Type u_3} [DecidableEq V] (E : Finset (Sym2 V)) (colour : Sym2 V → β) : Prop

Two distinct edges assigned the same colour have no common endpoint.

Equations

• LeanPool.Vizing.ColourClasses.ProperOn E colour = ∀ e ∈ E, ∀ f ∈ E, e ≠ f → colour e = colour f → Disjoint e.toFinset f.toFinset

theorem LeanPool.Vizing.ColourClasses.colourClass_pairwiseDisjoint_toFinset {β : Type u_2} [DecidableEq β] {V : Type u_3} [DecidableEq V] {E : Finset (Sym2 V)} {colour : Sym2 V → β} (hproper : ProperOn E colour) (b : β) : (↑(colourClass E colour b)).PairwiseDisjoint Sym2.toFinset

Every colour class of a proper edge colouring is a matching.