# 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`

is`V`

.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 an`n`

-partition. (a partition with at most`n`

parts).`SimpleGraph.Partitionable n`

is whether a given graph is`n`

-partite`SimpleGraph.Partition.toColoring`

creates colorings from partitions`SimpleGraph.Coloring.toPartition`

creates partitions from colorings

## Main statements #

`SimpleGraph.partitionable_iff_colorable`

is that`n`

-partitionability and`n`

-colorability are equivalent.

A `Partition`

of a simple graph `G`

is a structure constituted by

`parts`

: a set of subsets of the vertices`V`

of`G`

`isPartition`

: a proof that`parts`

is a proper partition of`V`

`independent`

: a proof that each element of`parts`

doesn't have a pair of adjacent vertices

`parts`

: a set of subsets of the vertices`V`

of`G`

.- isPartition : Setoid.IsPartition self.parts
`isPartition`

: a proof that`parts`

is a proper partition of`V`

. - independent : ∀ s ∈ self.parts, IsAntichain G.Adj s
`independent`

: a proof that each element of`parts`

doesn't have a pair of adjacent vertices.

## Instances For

`isPartition`

: a proof that `parts`

is a proper partition of `V`

.

`independent`

: a proof that each element of `parts`

doesn't have a pair of adjacent vertices.

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.

## Equations

- G.Partitionable n = ∃ (P : G.Partition), P.PartsCardLe n

## Instances For

The part in the partition that `v`

belongs to

## Equations

- P.partOfVertex v = Classical.choose ⋯

## Instances For

Create a coloring using the parts themselves as the colors. Each vertex is colored by the part it's contained in.

## Equations

- P.toColoring = SimpleGraph.Coloring.mk (fun (v : V) => ⟨P.partOfVertex v, ⋯⟩) ⋯

## Instances For

Like `SimpleGraph.Partition.toColoring`

but uses `Set V`

as the coloring type.

## Equations

- P.toColoring' = SimpleGraph.Coloring.mk P.partOfVertex ⋯

## Instances For

Creates a partition from a coloring.

## Equations

- C.toPartition = { parts := C.colorClasses, isPartition := ⋯, independent := ⋯ }

## Instances For

The partition where every vertex is in its own part.

## Equations

- SimpleGraph.instInhabitedPartition = { default := G.selfColoring.toPartition }