mathlib documentation

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:

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 simple_graph.partition {V : Type u} (G : simple_graph V) :
Type u

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
Instances for simple_graph.partition
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) :
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]

The partition where every vertex is in its own part.

Equations