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 #
-
simple_graph.partition
is a structure to represent a partition of a simple graph -
simple_graph.partition.parts_card_le
is whether a given partition is ann
-partition. (a partition with at mostn
parts). -
simple_graph.partitionable n
is whether a given graph isn
-partite -
simple_graph.partition.to_coloring
creates colorings from partitions -
simple_graph.coloring.to_partition
creates partitions from colorings
Main statements #
simple_graph.partitionable_iff_colorable
is thatn
-partitionability andn
-colorability are equivalent.
- parts : set (set V)
- is_partition : setoid.is_partition self.parts
- independent : ∀ (s : set V), s ∈ self.parts → is_antichain G.adj s
A partition
of a simple graph G
is a structure constituted by
parts
: a set of subsets of the verticesV
ofG
is_partition
: 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 simple_graph.partition
- simple_graph.partition.has_sizeof_inst
- simple_graph.partition.inhabited
Whether a partition P
has at most n
parts. A graph with a partition
satisfying this predicate called n
-partite. (See simple_graph.partitionable
.)
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.parts_card_le n
The part in the partition that v
belongs to
Equations
- P.part_of_vertex v = classical.some _
Create a coloring using the parts themselves as the colors. Each vertex is colored by the part it's contained in.
Equations
- P.to_coloring = simple_graph.coloring.mk (λ (v : V), ⟨P.part_of_vertex v, _⟩) _
Like simple_graph.partition.to_coloring
but uses set V
as the coloring type.
Equations
Creates a partition from a coloring.
Equations
- C.to_partition = {parts := C.color_classes, is_partition := _, independent := _}
The partition where every vertex is in its own part.