mathlibdocumentation

combinatorics.simple_graph.partition

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 #

• 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 an n-partition. (a partition with at most n parts).

• simple_graph.partitionable n is whether a given graph is n-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 that n-partitionability and n-colorability are equivalent.
structure simple_graph.partition {V : Type u} (G : simple_graph V) :
Type u
• parts : set (set V)
• is_partition :
• independent : ∀ (s : set V), s self.parts s

A partition of a simple graph G is a structure constituted by

• parts: a set of subsets of the vertices V of G
• is_partition: 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
def simple_graph.partition.parts_card_le {V : Type u} {G : simple_graph V} (P : G.partition) (n : ) :
Prop

Whether a partition P has at most n parts. A graph with a partition satisfying this predicate called n-partite. (See simple_graph.partitionable.)

Equations
def simple_graph.partitionable {V : Type u} (G : simple_graph V) (n : ) :
Prop

Whether a graph is n-partite, which is whether its vertex set can be partitioned in at most n independent sets.

Equations
def simple_graph.partition.part_of_vertex {V : Type u} {G : simple_graph V} (P : G.partition) (v : V) :
set V

The part in the partition that v belongs to

Equations
theorem simple_graph.partition.part_of_vertex_mem {V : Type u} {G : simple_graph V} (P : G.partition) (v : V) :
theorem simple_graph.partition.mem_part_of_vertex {V : Type u} {G : simple_graph V} (P : G.partition) (v : V) :
v
theorem simple_graph.partition.part_of_vertex_ne_of_adj {V : Type u} {G : simple_graph V} (P : G.partition) {v w : V} (h : G.adj v w) :
def simple_graph.partition.to_coloring {V : Type u} {G : simple_graph V} (P : G.partition) :

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

Equations
def simple_graph.partition.to_coloring' {V : Type u} {G : simple_graph V} (P : G.partition) :

Like simple_graph.partition.to_coloring but uses set V as the coloring type.

Equations
def simple_graph.coloring.to_partition {V : Type u} {G : simple_graph V} {α : Type v} (C : G.coloring α) :

Creates a partition from a coloring.

Equations
@[simp]
theorem simple_graph.coloring.to_partition_parts {V : Type u} {G : simple_graph V} {α : Type v} (C : G.coloring α) :
@[protected, instance]
def simple_graph.partition.inhabited {V : Type u} {G : simple_graph V} :
Equations
theorem simple_graph.partitionable_iff_colorable {V : Type u} {G : simple_graph V} {n : } :