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.
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
parts
: a set of subsets of the verticesV
ofG
. isPartition : Setoid.IsPartition self.parts
isPartition
: a proof thatparts
is a proper partition ofV
.  independent : ∀ s ∈ self.parts, IsAntichain G.Adj s
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
.)
Equations
 SimpleGraph.Partition.PartsCardLe P n = ∃ (h : Set.Finite P.parts), (Set.Finite.toFinset h).card ≤ n
Instances For
Whether a graph is n
partite, which is whether its vertex set
can be partitioned in at most n
independent sets.
Equations
 SimpleGraph.Partitionable G n = ∃ (P : SimpleGraph.Partition G), SimpleGraph.Partition.PartsCardLe P n
Instances For
The part in the partition that v
belongs to
Equations
 SimpleGraph.Partition.partOfVertex P v = Classical.choose (_ : ∃! (b : Set V), ∃! (x : b ∈ P.parts), v ∈ b)
Instances For
Create a coloring using the parts themselves as the colors. Each vertex is colored by the part it's contained in.
Equations
 One or more equations did not get rendered due to their size.
Instances For
Like SimpleGraph.Partition.toColoring
but uses Set V
as the coloring type.
Equations
 One or more equations did not get rendered due to their size.
Instances For
Creates a partition from a coloring.
Equations
 One or more equations did not get rendered due to their size.
Instances For
The partition where every vertex is in its own part.
Equations
 SimpleGraph.instInhabitedPartition = { default := SimpleGraph.Coloring.toPartition (SimpleGraph.selfColoring G) }