Refinement of a finite coloring (source code)

= Refinement of a finite coloring

A refinement of a <finite coloring> assigns different new colors whenever the original colors differ. A set <monochromatic> for the refinement is therefore <monochromatic> for the original coloring. Given colorings $\chi,\psi$, the product coloring $n\mapsto(\chi(n),\psi(n))$ refines both. This makes it possible to impose finitely many coloring obstructions simultaneously.