# mathlibdocumentation

combinatorics.simple_graph.basic

# Simple graphs #

This module defines simple graphs on a vertex type V as an irreflexive symmetric relation.

There is a basic API for locally finite graphs and for graphs with finitely many vertices.

## Main definitions #

• simple_graph is a structure for symmetric, irreflexive relations

• neighbor_set is the set of vertices adjacent to a given vertex

• common_neighbors is the intersection of the neighbor sets of two given vertices

• neighbor_finset is the finset of vertices adjacent to a given vertex, if neighbor_set is finite

• incidence_set is the set of edges containing a given vertex

• incidence_finset is the finset of edges containing a given vertex, if incidence_set is finite

## Implementation notes #

• A locally finite graph is one with instances ∀ v, fintype (G.neighbor_set v).

• Given instances decidable_rel G.adj and fintype V, then the graph is locally finite, too.

## Naming Conventions #

• If the vertex type of a graph is finite, we refer to its cardinality as card_verts.

TODO: This is the simplest notion of an unoriented graph. This should eventually fit into a more complete combinatorics hierarchy which includes multigraphs and directed graphs. We begin with simple graphs in order to start learning what the combinatorics hierarchy should look like.

TODO: Part of this would include defining, for example, subgraphs of a simple graph.

theorem simple_graph.ext {V : Type u} (x y : simple_graph V) (h : x.adj = y.adj) :
x = y
theorem simple_graph.ext_iff {V : Type u} (x y : simple_graph V) :
@[ext]
structure simple_graph (V : Type u) :
Type u
• adj : V → V → Prop
• sym : . "obviously"
• loopless : . "obviously"

A simple graph is an irreflexive symmetric relation adj on a vertex type V. The relation describes which pairs of vertices are adjacent. There is exactly one edge for every pair of adjacent edges; see simple_graph.edge_set for the corresponding edge set.

def simple_graph.from_rel {V : Type u} (r : V → V → Prop) :

Construct the simple graph induced by the given relation. It symmetrizes the relation and makes it irreflexive.

Equations
@[instance]
def simple_graph.fintype {V : Type u} [fintype V] :
Equations
@[simp]
theorem simple_graph.from_rel_adj {V : Type u} (r : V → V → Prop) (v w : V) :
v w v w (r v w r w v)
def complete_graph (V : Type u) :

The complete graph on a type V is the simple graph with all pairs of distinct vertices adjacent.

Equations
@[instance]
def simple_graph.inhabited (V : Type u) :
Equations
@[instance]
def complete_graph_adj_decidable (V : Type u) [decidable_eq V] :
Equations
def simple_graph.neighbor_set {V : Type u} (G : simple_graph V) (v : V) :
set V

G.neighbor_set v is the set of vertices adjacent to v in G.

Equations
@[instance]
def simple_graph.neighbor_set.mem_decidable {V : Type u} (G : simple_graph V) (v : V) [decidable_rel G.adj] :
Equations
theorem simple_graph.ne_of_adj {V : Type u} (G : simple_graph V) {a b : V} (hab : G.adj a b) :
a b
def simple_graph.edge_set {V : Type u} (G : simple_graph V) :
set (sym2 V)

The edges of G consist of the unordered pairs of vertices related by G.adj.

Equations
def simple_graph.incidence_set {V : Type u} (G : simple_graph V) (v : V) :
set (sym2 V)

The incidence_set is the set of edges incident to a given vertex.

Equations
theorem simple_graph.incidence_set_subset {V : Type u} (G : simple_graph V) (v : V) :
@[simp]
theorem simple_graph.mem_edge_set {V : Type u} (G : simple_graph V) {v w : V} :
(v, w) G.edge_set G.adj v w
theorem simple_graph.adj_iff_exists_edge {V : Type u} (G : simple_graph V) {v w : V} :
G.adj v w v w ∃ (e : sym2 V) (H : e G.edge_set), v e w e

Two vertices are adjacent iff there is an edge between them. The condition v ≠ w ensures they are different endpoints of the edge, which is necessary since when v = w the existential ∃ (e ∈ G.edge_set), v ∈ e ∧ w ∈ e is satisfied by every edge incident to v.

theorem simple_graph.edge_other_ne {V : Type u} (G : simple_graph V) {e : sym2 V} (he : e G.edge_set) {v : V} (h : v e) :
@[instance]
Equations
@[instance]
Equations
@[instance]
Equations

The edge_set of the graph as a finset.

Equations
@[simp]
theorem simple_graph.mem_edge_finset {V : Type u} (G : simple_graph V) [decidable_eq V] [fintype V] [decidable_rel G.adj] (e : sym2 V) :
@[simp]
@[simp]
theorem simple_graph.irrefl {V : Type u} (G : simple_graph V) {v : V} :
theorem simple_graph.edge_symm {V : Type u} (G : simple_graph V) (u v : V) :
theorem simple_graph.edge_symm' {V : Type u} (G : simple_graph V) {u v : V} (h : G.adj u v) :
@[simp]
theorem simple_graph.mem_neighbor_set {V : Type u} (G : simple_graph V) (v w : V) :
w G.neighbor_set v G.adj v w
@[simp]
theorem simple_graph.mem_incidence_set {V : Type u} (G : simple_graph V) (v w : V) :
theorem simple_graph.mem_incidence_iff_neighbor {V : Type u} (G : simple_graph V) {v w : V} :
theorem simple_graph.adj_incidence_set_inter {V : Type u} (G : simple_graph V) {v : V} {e : sym2 V} (he : e G.edge_set) (h : v e) :
= {e}
def simple_graph.common_neighbors {V : Type u} (G : simple_graph V) (v w : V) :
set V

The set of common neighbors between two vertices v and w in a graph G is the intersection of the neighbor sets of v and w.

Equations
theorem simple_graph.common_neighbors_eq {V : Type u} (G : simple_graph V) (v w : V) :
theorem simple_graph.mem_common_neighbors {V : Type u} (G : simple_graph V) {u v w : V} :
theorem simple_graph.common_neighbors_symm {V : Type u} (G : simple_graph V) (v w : V) :
w = v
theorem simple_graph.not_mem_common_neighbors_left {V : Type u} (G : simple_graph V) (v w : V) :
v w
theorem simple_graph.not_mem_common_neighbors_right {V : Type u} (G : simple_graph V) (v w : V) :
w w
@[instance]
Equations
def simple_graph.other_vertex_of_incident {V : Type u} (G : simple_graph V) [decidable_eq V] {v : V} {e : sym2 V} (h : e ) :
V

Given an edge incident to a particular vertex, get the other vertex on the edge.

Equations
theorem simple_graph.edge_mem_other_incident_set {V : Type u} (G : simple_graph V) [decidable_eq V] {v : V} {e : sym2 V} (h : e ) :
e
theorem simple_graph.incidence_other_prop {V : Type u} (G : simple_graph V) [decidable_eq V] {v : V} {e : sym2 V} (h : e ) :
@[simp]
theorem simple_graph.incidence_other_neighbor_edge {V : Type u} (G : simple_graph V) [decidable_eq V] {v w : V} (h : w G.neighbor_set v) :
@[simp]
@[simp]

There is an equivalence between the set of edges incident to a given vertex and the set of vertices adjacent to the vertex.

Equations

## Finiteness at a vertex #

This section contains definitions and lemmas concerning vertices that have finitely many adjacent vertices. We denote this condition by fintype (G.neighbor_set v).

We define G.neighbor_finset v to be the finset version of G.neighbor_set v. Use neighbor_finset_eq_filter to rewrite this definition as a filter.

def simple_graph.neighbor_finset {V : Type u} (G : simple_graph V) (v : V) [fintype (G.neighbor_set v)] :

G.neighbors v is the finset version of G.adj v in case G is locally finite at v.

Equations
@[simp]
theorem simple_graph.mem_neighbor_finset {V : Type u} (G : simple_graph V) (v : V) [fintype (G.neighbor_set v)] (w : V) :
def simple_graph.degree {V : Type u} (G : simple_graph V) (v : V) [fintype (G.neighbor_set v)] :

G.degree v is the number of vertices adjacent to v.

Equations
@[simp]
theorem simple_graph.card_neighbor_set_eq_degree {V : Type u} (G : simple_graph V) (v : V) [fintype (G.neighbor_set v)] :
= G.degree v
theorem simple_graph.degree_pos_iff_exists_adj {V : Type u} (G : simple_graph V) (v : V) [fintype (G.neighbor_set v)] :
0 < G.degree v ∃ (w : V), G.adj v w
@[instance]
Equations
def simple_graph.incidence_finset {V : Type u} (G : simple_graph V) (v : V) [fintype (G.neighbor_set v)] [decidable_eq V] :

This is the finset version of incidence_set.

Equations
@[simp]
theorem simple_graph.card_incidence_set_eq_degree {V : Type u} (G : simple_graph V) (v : V) [fintype (G.neighbor_set v)] [decidable_eq V] :
= G.degree v
@[simp]
theorem simple_graph.mem_incidence_finset {V : Type u} (G : simple_graph V) (v : V) [fintype (G.neighbor_set v)] [decidable_eq V] (e : sym2 V) :
e e
def simple_graph.locally_finite {V : Type u} (G : simple_graph V) :
Type u

A graph is locally finite if every vertex has a finite neighbor set.

Equations
def simple_graph.is_regular_of_degree {V : Type u} (G : simple_graph V) [G.locally_finite] (d : ) :
Prop

A locally finite simple graph is regular of degree d if every vertex has degree d.

Equations
theorem simple_graph.is_regular_of_degree_eq {V : Type u} (G : simple_graph V) [G.locally_finite] {d : } (h : G.is_regular_of_degree d) (v : V) :
G.degree v = d
@[instance]
Equations
@[simp]
theorem simple_graph.complete_graph_degree {V : Type u} [fintype V] [decidable_eq V] (v : V) :
.degree v =
def simple_graph.min_degree {V : Type u} (G : simple_graph V) [fintype V] [decidable_rel G.adj] :

The minimum degree of all vertices (and 0 if there are no vertices). The key properties of this are given in exists_minimal_degree_vertex, min_degree_le_degree and le_min_degree_of_forall_le_degree.

Equations
theorem simple_graph.exists_minimal_degree_vertex {V : Type u} (G : simple_graph V) [fintype V] [decidable_rel G.adj] [nonempty V] :
∃ (v : V), G.min_degree = G.degree v

There exists a vertex of minimal degree. Note the assumption of being nonempty is necessary, as the lemma implies there exists a vertex.

theorem simple_graph.min_degree_le_degree {V : Type u} (G : simple_graph V) [fintype V] [decidable_rel G.adj] (v : V) :

The minimum degree in the graph is at most the degree of any particular vertex.

theorem simple_graph.le_min_degree_of_forall_le_degree {V : Type u} (G : simple_graph V) [fintype V] [decidable_rel G.adj] [nonempty V] (k : ) (h : ∀ (v : V), k G.degree v) :

In a nonempty graph, if k is at most the degree of every vertex, it is at most the minimum degree. Note the assumption that the graph is nonempty is necessary as long as G.min_degree is defined to be a natural.

def simple_graph.max_degree {V : Type u} (G : simple_graph V) [fintype V] [decidable_rel G.adj] :

The maximum degree of all vertices (and 0 if there are no vertices). The key properties of this are given in exists_maximal_degree_vertex, degree_le_max_degree and max_degree_le_of_forall_degree_le.

Equations
theorem simple_graph.exists_maximal_degree_vertex {V : Type u} (G : simple_graph V) [fintype V] [decidable_rel G.adj] [nonempty V] :
∃ (v : V), G.max_degree = G.degree v

There exists a vertex of maximal degree. Note the assumption of being nonempty is necessary, as the lemma implies there exists a vertex.

theorem simple_graph.degree_le_max_degree {V : Type u} (G : simple_graph V) [fintype V] [decidable_rel G.adj] (v : V) :

The maximum degree in the graph is at least the degree of any particular vertex.

theorem simple_graph.max_degree_le_of_forall_degree_le {V : Type u} (G : simple_graph V) [fintype V] [decidable_rel G.adj] (k : ) (h : ∀ (v : V), G.degree v k) :

In a graph, if k is at least the degree of every vertex, then it is at least the maximum degree.

theorem simple_graph.degree_lt_card_verts {V : Type u} (G : simple_graph V) [fintype V] [decidable_rel G.adj] (v : V) :
G.degree v <

The maximum degree of a nonempty graph is less than the number of vertices. Note that the assumption that V is nonempty is necessary, as otherwise this would assert the existence of a natural less than zero.

theorem simple_graph.adj.card_common_neighbors_lt_degree {V : Type u} [fintype V] {G : simple_graph V} [decidable_rel G.adj] {v w : V} (h : G.adj v w) :

If the condition G.adj v w fails, then card_common_neighbors_le_degree is the best we can do in general.

## Complement of a simple graph #

This section contains definitions and lemmas concerning the complement of a simple graph.

def simple_graph.compl {V : Type u} (G : simple_graph V) :

We define compl G to be the simple_graph V such that no two adjacent vertices in G are adjacent in the complement, and every nonadjacent pair of vertices is adjacent (still ensuring that vertices are not adjacent to themselves.)

Equations
@[instance]
def simple_graph.has_compl {V : Type u} :
Equations
@[simp]
theorem simple_graph.compl_adj {V : Type u} (G : simple_graph V) (v w : V) :