# 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

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

• `simple_graph.common_neighbors` is the intersection of the neighbor sets of two given vertices

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

• `simple_graph.incidence_set` is the `set` of edges containing a given vertex

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

• `simple_graph.dart` is an ordered pair of adjacent vertices, thought of as being an orientated edge. These are also known as "half-edges" or "bonds."

• `simple_graph.hom`, `simple_graph.embedding`, and `simple_graph.iso` for graph homomorphisms, graph embeddings, and graph isomorphisms. Note that a graph embedding is a stronger notion than an injective graph homomorphism, since its image is an induced subgraph.

• `boolean_algebra` instance: Under the subgraph relation, `simple_graph` forms a `boolean_algebra`. In other words, this is the lattice of spanning subgraphs of the complete graph.

## Notations #

• `→g`, `↪g`, and `≃g` for graph homomorphisms, graph embeddings, and graph isomorphisms, respectively.

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

• Morphisms of graphs are abbreviations for `rel_hom`, `rel_embedding`, and `rel_iso`. To make use of pre-existing simp lemmas, definitions involving morphisms are abbreviations as well.

## Naming Conventions #

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

## Todo #

• Upgrade `simple_graph.boolean_algebra` to a `complete_boolean_algebra`.

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

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

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 vertices; see `simple_graph.edge_set` for the corresponding edge set.

Instances for `simple_graph`
@[protected, instance]
noncomputable def simple_graph.fintype {V : Type u} [fintype V] :
Equations
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
@[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. In `mathlib`, this is usually referred to as `⊤`.

Equations
def empty_graph (V : Type u) :

The graph with no edges on a given vertex type `V`. `mathlib` prefers the notation `⊥`.

Equations
def complete_bipartite_graph (V : Type u_1) (W : Type u_2) :

Two vertices are adjacent in the complete bipartite graph on two vertex types if and only if they are not from the same side. Bipartite graphs in general may be regarded as being subgraphs of one of these.

TODO also introduce complete multi-partite graphs, where the vertex type is a sigma type of an indexed family of vertex types

Equations
@[simp]
theorem complete_bipartite_graph_adj (V : Type u_1) (W : Type u_2) (v w : V W) :
@[protected, simp]
theorem simple_graph.irrefl {V : Type u} (G : simple_graph V) {v : V} :
theorem simple_graph.adj_comm {V : Type u} (G : simple_graph V) (u v : V) :
theorem simple_graph.adj_symm {V : Type u} (G : simple_graph V) {u v : V} (h : G.adj u v) :
theorem simple_graph.adj.symm {V : Type u} {G : simple_graph V} {u v : V} (h : G.adj u v) :
theorem simple_graph.ne_of_adj {V : Type u} (G : simple_graph V) {a b : V} (h : G.adj a b) :
a b
@[protected]
theorem simple_graph.adj.ne {V : Type u} {G : simple_graph V} {a b : V} (h : G.adj a b) :
a b
@[protected]
theorem simple_graph.adj.ne' {V : Type u} {G : simple_graph V} {a b : V} (h : G.adj a b) :
b a
theorem simple_graph.ne_of_adj_of_not_adj {V : Type u} (G : simple_graph V) {v w x : V} (h : G.adj v x) (hn : ¬G.adj w x) :
v w
def simple_graph.is_subgraph {V : Type u} (x y : simple_graph V) :
Prop

The relation that one `simple_graph` is a subgraph of another. Note that this should be spelled `≤`.

Equations
@[protected, instance]
def simple_graph.has_le {V : Type u} :
Equations
@[simp]
theorem simple_graph.is_subgraph_eq_le {V : Type u} :
@[protected, instance]
def simple_graph.has_sup {V : Type u} :

The supremum of two graphs `x ⊔ y` has edges where either `x` or `y` have edges.

Equations
@[simp]
theorem simple_graph.sup_adj {V : Type u} (x y : simple_graph V) (v w : V) :
(x y).adj v w x.adj v w y.adj v w
@[protected, instance]
def simple_graph.has_inf {V : Type u} :

The infimum of two graphs `x ⊓ y` has edges where both `x` and `y` have edges.

Equations
@[simp]
theorem simple_graph.inf_adj {V : Type u} (x y : simple_graph V) (v w : V) :
(x y).adj v w x.adj v w y.adj v w
@[protected, instance]
def simple_graph.has_compl {V : Type u} :

We define `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
@[simp]
theorem simple_graph.compl_adj {V : Type u} (G : simple_graph V) (v w : V) :
G.adj v w v w ¬G.adj v w
@[protected, instance]
def simple_graph.has_sdiff {V : Type u} :

The difference of two graphs `x \ y` has the edges of `x` with the edges of `y` removed.

Equations
@[simp]
theorem simple_graph.sdiff_adj {V : Type u} (x y : simple_graph V) (v w : V) :
(x \ y).adj v w x.adj v w ¬y.adj v w
@[protected, instance]
def simple_graph.boolean_algebra {V : Type u} :
Equations
@[simp]
theorem simple_graph.top_adj {V : Type u} (v w : V) :
.adj v w v w
@[simp]
theorem simple_graph.bot_adj {V : Type u} (v w : V) :
@[simp]
theorem simple_graph.complete_graph_eq_top (V : Type u) :
@[simp]
theorem simple_graph.empty_graph_eq_bot (V : Type u) :
@[protected, instance]
def simple_graph.inhabited (V : Type u) :
Equations
@[protected, instance]
def simple_graph.bot.adj_decidable (V : Type u) :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
def simple_graph.support {V : Type u} (G : simple_graph V) :
set V

`G.support` is the set of vertices that form edges in `G`.

Equations
theorem simple_graph.mem_support {V : Type u} (G : simple_graph V) {v : V} :
v G.support ∃ (w : V), G.adj v w
theorem simple_graph.support_mono {V : Type u} {G G' : simple_graph V} (h : G G') :
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
Instances for `↥simple_graph.neighbor_set`
@[protected, instance]
def simple_graph.neighbor_set.mem_decidable {V : Type u} (G : simple_graph V) (v : V) [decidable_rel G.adj] :
decidable_pred (λ (_x : V), _x G.neighbor_set v)
Equations
• = _.mpr (λ (a : V), (λ (a : V), G.adj v a))
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`.

The way `edge_set` is defined is such that `mem_edge_set` is proved by `refl`. (That is, `⟦(v, w)⟧ ∈ G.edge_set` is definitionally equal to `G.adj v w`.)

Equations
Instances for `↥simple_graph.edge_set`
@[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.adj_iff_exists_edge_coe {V : Type u} (G : simple_graph V) {a b : V} :
G.adj a b ∃ (e : (G.edge_set)), e = (a, b)
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) :
@[protected, instance]
Equations
@[protected, instance]
Equations

## Darts #

theorem simple_graph.dart.ext_iff {V : Type u} {G : simple_graph V} (x y : G.dart) :
theorem simple_graph.dart.ext {V : Type u} {G : simple_graph V} (x y : G.dart) (h : x.to_prod = y.to_prod) :
x = y
@[ext]
structure simple_graph.dart {V : Type u} (G : simple_graph V) :
Type u

A `dart` is an oriented edge, implemented as an ordered pair of adjacent vertices. This terminology comes from combinatorial maps, and they are also known as "half-edges" or "bonds."

Instances for `simple_graph.dart`
@[protected, instance]
def simple_graph.dart.decidable_eq {V : Type u} [a : decidable_eq V] (G : simple_graph V) :
def simple_graph.dart.fst {V : Type u} {G : simple_graph V} (d : G.dart) :
V

The first vertex for the dart.

def simple_graph.dart.snd {V : Type u} {G : simple_graph V} (d : G.dart) :
V

The second vertex for the dart.

@[protected, instance]
def simple_graph.dart.fintype {V : Type u} {G : simple_graph V} [fintype V] [decidable_rel G.adj] :
Equations
def simple_graph.dart.edge {V : Type u} {G : simple_graph V} (d : G.dart) :

The edge associated to the dart.

Equations
@[simp]
theorem simple_graph.dart.edge_mk {V : Type u} {G : simple_graph V} {p : V × V} (h : G.adj p.fst p.snd) :
{to_prod := p, is_adj := h}.edge = p
@[simp]
theorem simple_graph.dart.edge_mem {V : Type u} {G : simple_graph V} (d : G.dart) :
@[simp]
theorem simple_graph.dart.symm_to_prod {V : Type u} {G : simple_graph V} (d : G.dart) :
def simple_graph.dart.symm {V : Type u} {G : simple_graph V} (d : G.dart) :

The dart with reversed orientation from a given dart.

Equations
@[simp]
theorem simple_graph.dart.symm_mk {V : Type u} {G : simple_graph V} {p : V × V} (h : G.adj p.fst p.snd) :
{to_prod := p, is_adj := h}.symm = {to_prod := p.swap, is_adj := _}
@[simp]
theorem simple_graph.dart.edge_symm {V : Type u} {G : simple_graph V} (d : G.dart) :
@[simp]
theorem simple_graph.dart.edge_comp_symm {V : Type u} {G : simple_graph V} :
@[simp]
theorem simple_graph.dart.symm_symm {V : Type u} {G : simple_graph V} (d : G.dart) :
d.symm.symm = d
@[simp]
theorem simple_graph.dart.symm_involutive {V : Type u} {G : simple_graph V} :
theorem simple_graph.dart.symm_ne {V : Type u} {G : simple_graph V} (d : G.dart) :
d.symm d
theorem simple_graph.dart_edge_eq_iff {V : Type u} {G : simple_graph V} (d₁ d₂ : G.dart) :
d₁.edge = d₂.edge d₁ = d₂ d₁ = d₂.symm
theorem simple_graph.dart_edge_eq_mk_iff {V : Type u} {G : simple_graph V} {d : G.dart} {p : V × V} :
theorem simple_graph.dart_edge_eq_mk_iff' {V : Type u} {G : simple_graph V} {d : G.dart} {u v : V} :
def simple_graph.dart_adj {V : Type u} (G : simple_graph V) (d d' : G.dart) :
Prop

Two darts are said to be adjacent if they could be consecutive darts in a walk -- that is, the first dart's second vertex is equal to the second dart's first vertex.

Equations
def simple_graph.dart_of_neighbor_set {V : Type u} (G : simple_graph V) (v : V) (w : (G.neighbor_set v)) :

For a given vertex `v`, this is the bijective map from the neighbor set at `v` to the darts `d` with `d.fst = v`. -

Equations
@[simp]
theorem simple_graph.dart_of_neighbor_set_to_prod {V : Type u} (G : simple_graph V) (v : V) (w : (G.neighbor_set v)) :
w).to_prod = (v, w)
theorem simple_graph.dart_of_neighbor_set_injective {V : Type u} (G : simple_graph V) (v : V) :
@[protected, instance]
def simple_graph.dart.inhabited {V : Type u} (G : simple_graph V) [inhabited V]  :
Equations

### Incidence set #

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

Set of edges incident to a given vertex, aka incidence set.

Equations
Instances for `↥simple_graph.incidence_set`
theorem simple_graph.incidence_set_subset {V : Type u} (G : simple_graph V) (v : V) :
theorem simple_graph.mk_mem_incidence_set_iff {V : Type u} (G : simple_graph V) {a b c : V} :
(b, c) G.adj b c (a = b a = c)
theorem simple_graph.mk_mem_incidence_set_left_iff {V : Type u} (G : simple_graph V) {a b : V} :
(a, b) G.adj a b
theorem simple_graph.mk_mem_incidence_set_right_iff {V : Type u} (G : simple_graph V) {a b : V} :
(a, b) G.adj a b
theorem simple_graph.edge_mem_incidence_set_iff {V : Type u} (G : simple_graph V) {a : V} {e : (G.edge_set)} :
theorem simple_graph.incidence_set_inter_incidence_set_subset {V : Type u} (G : simple_graph V) {a b : V} (h : a b) :
{(a, b)}
theorem simple_graph.incidence_set_inter_incidence_set_of_adj {V : Type u} (G : simple_graph V) {a b : V} (h : G.adj a b) :
= {(a, b)}
theorem simple_graph.adj_of_mem_incidence_set {V : Type u} (G : simple_graph V) {a b : V} {e : sym2 V} (h : a b) (ha : e ) (hb : e ) :
theorem simple_graph.incidence_set_inter_incidence_set_of_not_adj {V : Type u} (G : simple_graph V) {a b : V} (h : ¬G.adj a b) (hn : a b) :
@[protected, instance]
def simple_graph.decidable_mem_incidence_set {V : Type u} (G : simple_graph V) [decidable_eq V] [decidable_rel G.adj] (v : V) :
decidable_pred (λ (_x : sym2 V), _x G.incidence_set v)
Equations
def simple_graph.edge_finset {V : Type u} (G : simple_graph V) [fintype (G.edge_set)] :

The `edge_set` of the graph as a `finset`.

Equations
@[simp]
theorem simple_graph.mem_edge_finset {V : Type u} (G : simple_graph V) [fintype (G.edge_set)] (e : sym2 V) :
theorem simple_graph.edge_finset_card {V : Type u} (G : simple_graph V) [fintype (G.edge_set)] :
@[simp]
theorem simple_graph.edge_set_univ_card {V : Type u} (G : simple_graph V) [fintype (G.edge_set)] :
@[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_neighbor_set' {V : Type u} (G : simple_graph V) (v w : V) :
G.neighbor_set v w G.adj v w
@[simp]
theorem simple_graph.mem_incidence_set {V : Type u} (G : simple_graph V) (v w : V) :
(v, w) G.adj v w
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}
theorem simple_graph.neighbor_set_compl {V : Type u} (G : simple_graph V) (v : V) :
= (G.neighbor_set v) \ {v}
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} :
u w G.adj v u G.adj w u
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
@[protected, instance]
def simple_graph.decidable_mem_common_neighbors {V : Type u} (G : simple_graph V) [decidable_rel G.adj] (v w : V) :
decidable_pred (λ (_x : V), _x G.common_neighbors v w)
Equations
theorem simple_graph.common_neighbors_top_eq {V : Type u} {v w : V} :
= set.univ \ {v, w}
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_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

## Edge deletion #

def simple_graph.delete_edges {V : Type u} (G : simple_graph V) (s : set (sym2 V)) :

Given a set of vertex pairs, remove all of the corresponding edges from the graph's edge set, if present.

See also: `simple_graph.subgraph.delete_edges`.

Equations
@[simp]
theorem simple_graph.delete_edges_adj {V : Type u} (G : simple_graph V) (s : set (sym2 V)) (v w : V) :
(G.delete_edges s).adj v w G.adj v w (v, w) s
theorem simple_graph.sdiff_eq_delete_edges {V : Type u} (G G' : simple_graph V) :
theorem simple_graph.compl_eq_delete_edges {V : Type u} (G : simple_graph V) :
@[simp]
theorem simple_graph.delete_edges_delete_edges {V : Type u} (G : simple_graph V) (s s' : set (sym2 V)) :
@[simp]
theorem simple_graph.delete_edges_empty_eq {V : Type u} (G : simple_graph V) :
= G
@[simp]
theorem simple_graph.delete_edges_univ_eq {V : Type u} (G : simple_graph V) :
theorem simple_graph.delete_edges_le {V : Type u} (G : simple_graph V) (s : set (sym2 V)) :
theorem simple_graph.delete_edges_le_of_le {V : Type u} (G : simple_graph V) {s s' : set (sym2 V)} (h : s s') :

## 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
theorem simple_graph.neighbor_finset_def {V : Type u} (G : simple_graph V) (v : V) [fintype (G.neighbor_set v)] :
@[simp]
theorem simple_graph.mem_neighbor_finset {V : Type u} (G : simple_graph V) (v : V) [fintype (G.neighbor_set v)] (w : V) :
w G.adj v w
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
theorem simple_graph.degree_compl {V : Type u} (G : simple_graph V) (v : V) [fintype (G.neighbor_set v)] [fintype (G.neighbor_set v)] [fintype V] :
@[protected, 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.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
@[protected, instance]
Equations
theorem simple_graph.neighbor_finset_compl {V : Type u} (G : simple_graph V) [fintype V] [decidable_eq V] [decidable_rel G.adj] (v : V) :
@[simp]
theorem simple_graph.complete_graph_degree {V : Type u} [fintype V] [decidable_eq V] (v : V) :
theorem simple_graph.bot_degree {V : Type u} [fintype V] (v : 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 number 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.

theorem simple_graph.card_common_neighbors_top {V : Type u} [fintype V] [decidable_eq V] {v w : V} (h : v w) :
=
def simple_graph.hom {V : Type u} {W : Type v} (G : simple_graph V) (G' : simple_graph W) :
Type (max u v)

A graph homomorphism is a map on vertex sets that respects adjacency relations.

The notation `G →g G'` represents the type of graph homomorphisms.

def simple_graph.embedding {V : Type u} {W : Type v} (G : simple_graph V) (G' : simple_graph W) :
Type (max u v)

A graph embedding is an embedding `f` such that for vertices `v w : V`, `G.adj f(v) f(w) ↔ G.adj v w`. Its image is an induced subgraph of G'.

The notation `G ↪g G'` represents the type of graph embeddings.

def simple_graph.iso {V : Type u} {W : Type v} (G : simple_graph V) (G' : simple_graph W) :
Type (max u v)

A graph isomorphism is an bijective map on vertex sets that respects adjacency relations.

The notation `G ≃g G'` represents the type of graph isomorphisms.

def simple_graph.hom.id {V : Type u} {G : simple_graph V} :
G →g G

The identity homomorphism from a graph to itself.

theorem simple_graph.hom.map_adj {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G →g G') {v w : V} (h : G.adj v w) :
G'.adj (f v) (f w)
theorem simple_graph.hom.map_mem_edge_set {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G →g G') {e : sym2 V} (h : e G.edge_set) :
theorem simple_graph.hom.apply_mem_neighbor_set {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G →g G') {v w : V} (h : w G.neighbor_set v) :
f w G'.neighbor_set (f v)
def simple_graph.hom.map_edge_set {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G →g G') (e : (G.edge_set)) :

The map between edge sets induced by a homomorphism. The underlying map on edges is given by `sym2.map`.

Equations
@[simp]
theorem simple_graph.hom.map_edge_set_coe {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G →g G') (e : (G.edge_set)) :
@[simp]
theorem simple_graph.hom.map_neighbor_set_coe {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G →g G') (v : V) (w : (G.neighbor_set v)) :
def simple_graph.hom.map_neighbor_set {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G →g G') (v : V) (w : (G.neighbor_set v)) :

The map between neighbor sets induced by a homomorphism.

Equations
def simple_graph.hom.map_dart {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G →g G') (d : G.dart) :
G'.dart

The map between darts induced by a homomorphism.

Equations
@[simp]
theorem simple_graph.hom.map_dart_apply {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G →g G') (d : G.dart) :
f.map_dart d = {to_prod := f d.to_prod, is_adj := _}
def simple_graph.hom.map_spanning_subgraphs {V : Type u} {G G' : simple_graph V} (h : G G') :
G →g G'

The induced map for spanning subgraphs, which is the identity on vertices.

Equations
theorem simple_graph.hom.map_edge_set.injective {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G →g G') (hinj : function.injective f) :
def simple_graph.hom.comp {V : Type u} {W : Type v} {X : Type w} {G : simple_graph V} {G' : simple_graph W} {G'' : simple_graph X} (f' : G' →g G'') (f : G →g G') :
G →g G''

Composition of graph homomorphisms.

@[simp]
theorem simple_graph.hom.coe_comp {V : Type u} {W : Type v} {X : Type w} {G : simple_graph V} {G' : simple_graph W} {G'' : simple_graph X} (f' : G' →g G'') (f : G →g G') :
(f'.comp f) = f' f
def simple_graph.embedding.refl {V : Type u} {G : simple_graph V} :
G ↪g G

The identity embedding from a graph to itself.

def simple_graph.embedding.to_hom {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G ↪g G') :
G →g G'

An embedding of graphs gives rise to a homomorphism of graphs.

theorem simple_graph.embedding.map_adj_iff {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G ↪g G') {v w : V} :
G'.adj (f v) (f w) G.adj v w
theorem simple_graph.embedding.map_mem_edge_set_iff {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G ↪g G') {e : sym2 V} :
theorem simple_graph.embedding.apply_mem_neighbor_set_iff {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G ↪g G') {v w : V} :
@[simp]
theorem simple_graph.embedding.map_edge_set_apply {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G ↪g G') (e : (G.edge_set)) :
def simple_graph.embedding.map_edge_set {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G ↪g G') :

A graph embedding induces an embedding of edge sets.

Equations
def simple_graph.embedding.map_neighbor_set {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G ↪g G') (v : V) :

A graph embedding induces an embedding of neighbor sets.

Equations
@[simp]
theorem simple_graph.embedding.map_neighbor_set_apply_coe {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G ↪g G') (v : V) (w : (G.neighbor_set v)) :
def simple_graph.embedding.complete_graph.of_embedding {α : Type u_1} {β : Type u_2} (f : α β) :

Embeddings of types induce embeddings of complete graphs on those types.

Equations
def simple_graph.embedding.comp {V : Type u} {W : Type v} {X : Type w} {G : simple_graph V} {G' : simple_graph W} {G'' : simple_graph X} (f' : G' ↪g G'') (f : G ↪g G') :
G ↪g G''

Composition of graph embeddings.

@[simp]
theorem simple_graph.embedding.coe_comp {V : Type u} {W : Type v} {X : Type w} {G : simple_graph V} {G' : simple_graph W} {G'' : simple_graph X} (f' : G' ↪g G'') (f : G ↪g G') :
(f'.comp f) = f' f
def simple_graph.iso.refl {V : Type u} {G : simple_graph V} :
G ≃g G

The identity isomorphism of a graph with itself.

def simple_graph.iso.to_embedding {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G ≃g G') :
G ↪g G'

An isomorphism of graphs gives rise to an embedding of graphs.

def simple_graph.iso.to_hom {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G ≃g G') :
G →g G'

An isomorphism of graphs gives rise to a homomorphism of graphs.

def simple_graph.iso.symm {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G ≃g G') :
G' ≃g G

The inverse of a graph isomorphism. -

theorem simple_graph.iso.map_adj_iff {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G ≃g G') {v w : V} :
G'.adj (f v) (f w) G.adj v w
theorem simple_graph.iso.map_mem_edge_set_iff {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G ≃g G') {e : sym2 V} :
theorem simple_graph.iso.apply_mem_neighbor_set_iff {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G ≃g G') {v w : V} :
@[simp]
theorem simple_graph.iso.map_edge_set_apply {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G ≃g G') (e : (G.edge_set)) :
def simple_graph.iso.map_edge_set {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G ≃g G') :

An isomorphism of graphs induces an equivalence of edge sets.

Equations
@[simp]
theorem simple_graph.iso.map_edge_set_symm_apply {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G ≃g G') (e : (G'.edge_set)) :
@[simp]
theorem simple_graph.iso.map_neighbor_set_symm_apply_coe {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G ≃g G') (v : V) (w : (G'.neighbor_set (f v))) :
def simple_graph.iso.map_neighbor_set {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G ≃g G') (v : V) :

A graph isomorphism induces an equivalence of neighbor sets.

Equations
@[simp]
theorem simple_graph.iso.map_neighbor_set_apply_coe {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} (f : G ≃g G') (v : V) (w : (G.neighbor_set v)) :
theorem simple_graph.iso.card_eq_of_iso {V : Type u} {W : Type v} {G : simple_graph V} {G' : simple_graph W} [fintype V] [fintype W] (f : G ≃g G') :
def simple_graph.iso.comp {V : Type u} {W : Type v} {X : Type w} {G : simple_graph V} {G' : simple_graph W} {G'' : simple_graph X} (f' : G' ≃g G'') (f : G ≃g G') :
G ≃g G''

Composition of graph isomorphisms.

@[simp]
theorem simple_graph.iso.coe_comp {V : Type u} {W : Type v} {X : Type w} {G : simple_graph V} {G' : simple_graph W} {G'' : simple_graph X} (f' : G' ≃g G'') (f : G ≃g G') :
(f'.comp f) = f' f