Graph Coloring #
This module defines colorings of simple graphs (also known as proper colorings in the literature). A graph coloring is the attribution of "colors" to all of its vertices such that adjacent vertices have different colors. A coloring can be represented as a homomorphism into a complete graph, whose vertices represent the colors.
Main definitions #
G.Coloring αis the type of
α-colorings of a simple graph
αbeing the set of available colors. The type is defined to be homomorphisms from
Ginto the complete graph on
α, and colorings have a coercion to
V → α.
G.Colorable nis the proposition that
n-colorable, which is whether there exists a coloring with at most n colors.
G.chromaticNumberis the minimal
0if it cannot be colored with finitely many colors.
C.colorClassesis the set containing all color classes.
Gather material from:
develop API for partial colorings, likely as colorings of subgraphs (
Construct a term of
SimpleGraph.Coloring using a function that
assigns vertices to colors and a proof that it is as proper coloring.
(Note: this is a definitionally the constructor for
but with a syntactically better proper coloring hypothesis.)
There is a noncomputable embedding of
β has at least as large a cardinality as