Graph partitions #
This module provides an interface for dealing with partitions on simple graphs. A partition of
a graph G
, with vertices V
, is a set P
of disjoint nonempty subsets of V
such that:

The union of the subsets in
P
isV
. 
Each element of
P
is an independent set. (Each subset contains no pair of adjacent vertices.)
Graph partitions are graph colorings that do not name their colors. They are adjoint in the following sense. Given a graph coloring, there is an associated partition from the set of color classes, and given a partition, there is an associated graph coloring from using the partition's subsets as colors. Going from graph colorings to partitions and back makes a coloring "canonical": all colors are given a canonical name and unused colors are removed. Going from partitions to graph colorings and back is the identity.
Main definitions #

SimpleGraph.Partition
is a structure to represent a partition of a simple graph 
SimpleGraph.Partition.PartsCardLe
is whether a given partition is ann
partition. (a partition with at mostn
parts). 
SimpleGraph.Partitionable n
is whether a given graph isn
partite 
SimpleGraph.Partition.toColoring
creates colorings from partitions 
SimpleGraph.Coloring.toPartition
creates partitions from colorings
Main statements #
SimpleGraph.partitionable_iff_colorable
is thatn
partitionability andn
colorability are equivalent.
parts
: a set of subsets of the verticesV
ofG
. isPartition : Setoid.IsPartition s.parts
isPartition
: a proof thatparts
is a proper partition ofV
.  independent : ∀ (s_1 : Set V), s_1 ∈ s.parts → IsAntichain G.Adj s_1
independent
: a proof that each element ofparts
doesn't have a pair of adjacent vertices.
A Partition
of a simple graph G
is a structure constituted by
parts
: a set of subsets of the verticesV
ofG
isPartition
: a proof thatparts
is a proper partition ofV
independent
: a proof that each element ofparts
doesn't have a pair of adjacent vertices
Instances For
Whether a partition P
has at most n
parts. A graph with a partition
satisfying this predicate called n
partite. (See SimpleGraph.Partitionable
.)
Instances For
Whether a graph is n
partite, which is whether its vertex set
can be partitioned in at most n
independent sets.
Instances For
The part in the partition that v
belongs to
Instances For
Create a coloring using the parts themselves as the colors. Each vertex is colored by the part it's contained in.
Instances For
Like SimpleGraph.Partition.toColoring
but uses Set V
as the coloring type.
Instances For
Creates a partition from a coloring.
Instances For
The partition where every vertex is in its own part.