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:

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 #

Main statements #

structure SimpleGraph.Partition {V : Type u} (G : SimpleGraph V) :

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
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.