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
homo, embedding, and 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.

source

theorem simple_graph.ext {V : Type u} (x y : simple_graph V) (h : x.adj = y.adj) :

x = y

source

theorem simple_graph.ext_iff {V : Type u} (x y : simple_graph V) :

x = y ↔ x.adj = y.adj

source

@[ext]

structure simple_graph (V : Type u) :

Type u

adj : V → V → Prop
sym : symmetric c.adj . "obviously"
loopless : irreflexive c.adj . "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.

source

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

simple_graph V

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

Equations

simple_graph.from_rel r = {adj := λ (a b : V), a ≠ b ∧ (r a b ∨ r b a), sym := _, loopless := _}

source

@[instance]

def simple_graph.fintype {V : Type u} [fintype V] :

fintype (simple_graph V)

Equations

simple_graph.fintype = fintype.of_injective simple_graph.adj simple_graph.ext

source

@[simp]

theorem simple_graph.from_rel_adj {V : Type u} (r : V → V → Prop) (v w : V) :

(simple_graph.from_rel r).adj v w ↔ v ≠ w ∧ (r v w ∨ r w v)

source

def complete_graph (V : Type u) :

simple_graph V

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

complete_graph V = {adj := ne V, sym := _, loopless := _}

source

def empty_graph (V : Type u) :

simple_graph V

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

Equations

empty_graph V = {adj := λ (i j : V), false, sym := _, loopless := _}

source

@[simp]

theorem simple_graph.irrefl {V : Type u} (G : simple_graph V) {v : V} :

¬G.adj v v

source

theorem simple_graph.adj_comm {V : Type u} (G : simple_graph V) (u v : V) :

G.adj u v ↔ G.adj v u

source

theorem simple_graph.adj_symm {V : Type u} (G : simple_graph V) {u v : V} (h : G.adj u v) :

G.adj v u

source

theorem simple_graph.ne_of_adj {V : Type u} (G : simple_graph V) {a b : V} (hab : G.adj a b) :

a ≠ b

source

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

x.is_subgraph y = ∀ ⦃v w : V⦄, x.adj v w → y.adj v w

source

@[instance]

def simple_graph.has_le {V : Type u} :

has_le (simple_graph V)

Equations

simple_graph.has_le = {le := simple_graph.is_subgraph V}

source

@[simp]

theorem simple_graph.is_subgraph_eq_le {V : Type u} :

simple_graph.is_subgraph = has_le.le

source

@[instance]

def simple_graph.has_sup {V : Type u} :

has_sup (simple_graph V)

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

Equations

simple_graph.has_sup = {sup := λ (x y : simple_graph V), {adj := x.adj ⊔ y.adj, sym := _, loopless := _}}

source

@[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

source

@[instance]

def simple_graph.has_inf {V : Type u} :

has_inf (simple_graph V)

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

Equations

simple_graph.has_inf = {inf := λ (x y : simple_graph V), {adj := x.adj ⊓ y.adj, sym := _, loopless := _}}

source

@[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

source

@[instance]

def simple_graph.has_compl {V : Type u} :

has_compl (simple_graph V)

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

simple_graph.has_compl = {compl := λ (G : simple_graph V), {adj := λ (v w : V), v ≠ w ∧ ¬G.adj v w, sym := _, loopless := _}}

source

@[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

source

@[instance]

def simple_graph.has_sdiff {V : Type u} :

has_sdiff (simple_graph V)

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

Equations

simple_graph.has_sdiff = {sdiff := λ (x y : simple_graph V), {adj := x.adj \ y.adj, sym := _, loopless := _}}

source

@[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

source

@[instance]

def simple_graph.boolean_algebra {V : Type u} :

boolean_algebra (simple_graph V)

Equations

simple_graph.boolean_algebra = {bot := empty_graph V, le := has_le.le simple_graph.has_le, lt := partial_order.lt (partial_order.lift simple_graph.adj simple_graph.ext), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _, sup := has_sup.sup simple_graph.has_sup, le_sup_left := _, le_sup_right := _, sup_le := _, inf := has_inf.inf simple_graph.has_inf, inf_le_left := _, inf_le_right := _, le_inf := _, le_sup_inf := _, sdiff := sdiff simple_graph.has_sdiff, sup_inf_sdiff := _, inf_inf_sdiff := _, top := complete_graph V, le_top := _, compl := compl simple_graph.has_compl, inf_compl_le_bot := _, top_le_sup_compl := _, sdiff_eq := _}

source

@[simp]

theorem simple_graph.top_adj {V : Type u} (v w : V) :

⊤.adj v w ↔ v ≠ w

source

@[simp]

theorem simple_graph.bot_adj {V : Type u} (v w : V) :

⊥.adj v w ↔ false

source

@[simp]

theorem simple_graph.complete_graph_eq_top (V : Type u) :

complete_graph V = ⊤

source

@[simp]

theorem simple_graph.empty_graph_eq_bot (V : Type u) :

empty_graph V = ⊥

source

@[instance]

def simple_graph.inhabited (V : Type u) :

inhabited (simple_graph V)

Equations

simple_graph.inhabited V = {default := ⊤}

source

@[instance]

def simple_graph.bot.adj_decidable (V : Type u) :

decidable_rel ⊥.adj

Equations

simple_graph.bot.adj_decidable V = λ (v w : V), decidable.false

source

@[instance]

def simple_graph.sup.adj_decidable (V : Type u) (G H : simple_graph V) [decidable_rel G.adj] [decidable_rel H.adj] :

decidable_rel (G ⊔ H).adj

Equations

simple_graph.sup.adj_decidable V G H = λ (v w : V), or.decidable

source

@[instance]

def simple_graph.inf.adj_decidable (V : Type u) (G H : simple_graph V) [decidable_rel G.adj] [decidable_rel H.adj] :

decidable_rel (G ⊓ H).adj

Equations

simple_graph.inf.adj_decidable V G H = λ (v w : V), and.decidable

source

@[instance]

def simple_graph.sdiff.adj_decidable (V : Type u) (G H : simple_graph V) [decidable_rel G.adj] [decidable_rel H.adj] :

decidable_rel (G \ H).adj

Equations

simple_graph.sdiff.adj_decidable V G H = λ (v w : V), and.decidable

source

@[instance]

def simple_graph.top.adj_decidable (V : Type u) [decidable_eq V] :

decidable_rel ⊤.adj

Equations

simple_graph.top.adj_decidable V = λ (v w : V), not.decidable

source

@[instance]

def simple_graph.compl.adj_decidable (V : Type u) (G : simple_graph V) [decidable_rel G.adj] [decidable_eq V] :

decidable_rel Gᶜ.adj

Equations

simple_graph.compl.adj_decidable V G = λ (v w : V), and.decidable

source

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

G.neighbor_set v = set_of (G.adj v)

source

@[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

simple_graph.neighbor_set.mem_decidable G v = _.mpr (λ (a : V), set.decidable_set_of (λ (a : V), G.adj v a) a)

source

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

G.edge_set = sym2.from_rel _

source

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

G.incidence_set v = {e ∈ G.edge_set | v ∈ e}

source

theorem simple_graph.incidence_set_subset {V : Type u} (G : simple_graph V) (v : V) :

G.incidence_set v ⊆ G.edge_set

source

@[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

source

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.

source

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) :

sym2.mem.other h ≠ v

source

@[instance]

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

decidable_pred (λ (_x : sym2 V), _x ∈ G.edge_set)

Equations

G.decidable_mem_edge_set = sym2.from_rel.decidable_pred _

source

@[instance]

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

fintype ↥(G.edge_set)

Equations

G.edges_fintype = subtype.fintype (λ (x : sym2 V), x ∈ G.edge_set)

source

@[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

G.decidable_mem_incidence_set v = λ (e : sym2 V), and.decidable

source

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

finset (sym2 V)

The edge_set of the graph as a finset.

Equations

G.edge_finset = G.edge_set.to_finset

source

@[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) :

e ∈ G.edge_finset ↔ e ∈ G.edge_set

source

@[simp]

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

finset.univ.card = G.edge_finset.card

source

@[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

source

@[simp]

theorem simple_graph.mem_incidence_set {V : Type u} (G : simple_graph V) (v w : V) :

⟦(v, w)⟧ ∈ G.incidence_set v ↔ G.adj v w

source

theorem simple_graph.mem_incidence_iff_neighbor {V : Type u} (G : simple_graph V) {v w : V} :

⟦(v, w)⟧ ∈ G.incidence_set v ↔ w ∈ G.neighbor_set v

source

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) :

G.incidence_set v ∩ G.incidence_set (sym2.mem.other h) = {e}

source

theorem simple_graph.compl_neighbor_set_disjoint {V : Type u} (G : simple_graph V) (v : V) :

disjoint (G.neighbor_set v) (Gᶜ.neighbor_set v)

source

theorem simple_graph.neighbor_set_union_compl_neighbor_set_eq {V : Type u} (G : simple_graph V) (v : V) :

G.neighbor_set v ∪ Gᶜ.neighbor_set v = {v}ᶜ

source

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

G.common_neighbors v w = G.neighbor_set v ∩ G.neighbor_set w

source

theorem simple_graph.common_neighbors_eq {V : Type u} (G : simple_graph V) (v w : V) :

G.common_neighbors v w = G.neighbor_set v ∩ G.neighbor_set w

source

theorem simple_graph.mem_common_neighbors {V : Type u} (G : simple_graph V) {u v w : V} :

u ∈ G.common_neighbors v w ↔ G.adj v u ∧ G.adj w u

source

theorem simple_graph.common_neighbors_symm {V : Type u} (G : simple_graph V) (v w : V) :

G.common_neighbors v w = G.common_neighbors w v

source

theorem simple_graph.not_mem_common_neighbors_left {V : Type u} (G : simple_graph V) (v w : V) :

v ∉ G.common_neighbors v w

source

theorem simple_graph.not_mem_common_neighbors_right {V : Type u} (G : simple_graph V) (v w : V) :

w ∉ G.common_neighbors v w

source

theorem simple_graph.common_neighbors_subset_neighbor_set {V : Type u} (G : simple_graph V) (v w : V) :

G.common_neighbors v w ⊆ G.neighbor_set v

source

@[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

G.decidable_mem_common_neighbors v w = λ (a : V), and.decidable

source

def simple_graph.other_vertex_of_incident {V : Type u} (G : simple_graph V) [decidable_eq V] {v : V} {e : sym2 V} (h : e ∈ G.incidence_set v) :

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

Equations

G.other_vertex_of_incident h = sym2.mem.other' _

source

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 ∈ G.incidence_set v) :

e ∈ G.incidence_set (G.other_vertex_of_incident h)

source

theorem simple_graph.incidence_other_prop {V : Type u} (G : simple_graph V) [decidable_eq V] {v : V} {e : sym2 V} (h : e ∈ G.incidence_set v) :

G.other_vertex_of_incident h ∈ G.neighbor_set v

source

@[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) :

G.other_vertex_of_incident _ = w

source

@[simp]

theorem simple_graph.incidence_set_equiv_neighbor_set_apply_coe {V : Type u} (G : simple_graph V) [decidable_eq V] (v : V) (e : ↥(G.incidence_set v)) :

↑(⇑(G.incidence_set_equiv_neighbor_set v) e) = G.other_vertex_of_incident _

source

@[simp]

theorem simple_graph.incidence_set_equiv_neighbor_set_symm_apply_coe {V : Type u} (G : simple_graph V) [decidable_eq V] (v : V) (w : ↥(G.neighbor_set v)) :

↑(⇑((G.incidence_set_equiv_neighbor_set v).symm) w) = ⟦(v, w.val)⟧

source

def simple_graph.incidence_set_equiv_neighbor_set {V : Type u} (G : simple_graph V) [decidable_eq V] (v : V) :

↥(G.incidence_set v) ≃ ↥(G.neighbor_set v)

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

Equations

G.incidence_set_equiv_neighbor_set v = {to_fun := λ (e : ↥(G.incidence_set v)), ⟨G.other_vertex_of_incident _, _⟩, inv_fun := λ (w : ↥(G.neighbor_set v)), ⟨⟦(v, w.val)⟧, _⟩, left_inv := _, right_inv := _}

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.

source

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

finset V

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

Equations

G.neighbor_finset v = (G.neighbor_set v).to_finset

source

@[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.neighbor_finset v ↔ G.adj v w

source

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

G.degree v = (G.neighbor_finset v).card

source

@[simp]

theorem simple_graph.card_neighbor_set_eq_degree {V : Type u} (G : simple_graph V) (v : V) [fintype ↥(G.neighbor_set v)] :

fintype.card ↥(G.neighbor_set v) = G.degree v

source

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

source

@[instance]

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

fintype ↥(G.incidence_set v)

Equations

G.incidence_set_fintype v = fintype.of_equiv ↥(G.neighbor_set v) (G.incidence_set_equiv_neighbor_set v).symm

source

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

finset (sym2 V)

This is the finset version of incidence_set.

Equations

G.incidence_finset v = (G.incidence_set v).to_finset

source

@[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] :

fintype.card ↥(G.incidence_set v) = G.degree v

source

@[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 ∈ G.incidence_finset v ↔ e ∈ G.incidence_set v

source

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

G.locally_finite = Π (v : V), fintype ↥(G.neighbor_set v)

source

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

G.is_regular_of_degree d = ∀ (v : V), G.degree v = d

source

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

source

@[instance]

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

fintype ↥(G.neighbor_set v)

Equations

G.neighbor_set_fintype v = subtype.fintype (λ (x : V), x ∈ G.neighbor_set v)

source

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

G.neighbor_finset v = finset.filter (G.adj v) finset.univ

source

@[simp]

theorem simple_graph.complete_graph_degree {V : Type u} [fintype V] [decidable_eq V] (v : V) :

⊤.degree v = fintype.card V - 1

source

theorem simple_graph.complete_graph_is_regular {V : Type u} [fintype V] [decidable_eq V] :

⊤.is_regular_of_degree (fintype.card V - 1)

source

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

G.min_degree = (finset.image (λ (v : V), G.degree v) finset.univ).min.get_or_else 0

source

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.

source

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

G.min_degree ≤ G.degree v

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

source

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) :

k ≤ G.min_degree

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.

source

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

G.max_degree = (finset.image (λ (v : V), G.degree v) finset.univ).max.get_or_else 0

source

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.

source

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

G.degree v ≤ G.max_degree

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

source

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) :

G.max_degree ≤ k

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

source

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 < fintype.card V

source

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

G.max_degree < fintype.card 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.

source

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

fintype.card ↥(G.common_neighbors v w) ≤ G.degree v

source

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

fintype.card ↥(G.common_neighbors v w) ≤ G.degree w

source

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

fintype.card ↥(G.common_neighbors v w) < fintype.card V

source

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) :

fintype.card ↥(G.common_neighbors v w) < G.degree v

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

source

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.

source

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.

source

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.

source

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

G →g G

The identity homomorphism from a graph to itself.

source

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)

source

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) :

sym2.map ⇑f e ∈ G'.edge_set

source

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)

source

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)) :

↥(G'.edge_set)

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

Equations

f.map_edge_set e = ⟨sym2.map ⇑f ↑e, _⟩

source

@[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)) :

↑(f.map_edge_set e) = sym2.map ⇑f ↑e

source

@[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)) :

↑(f.map_neighbor_set v w) = ⇑f ↑w

source

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)) :

↥(G'.neighbor_set (⇑f v))

The map between neighbor sets induced by a homomorphism.

Equations

f.map_neighbor_set v w = ⟨⇑f ↑w, _⟩

source

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) :

function.injective f.map_edge_set

source

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.

source

@[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

source

def simple_graph.embedding.refl {V : Type u} {G : simple_graph V} :

G ↪g G

The identity embedding from a graph to itself.

source

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.

source

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

source

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} :

sym2.map ⇑f e ∈ G'.edge_set ↔ e ∈ G.edge_set

source

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} :

⇑f w ∈ G'.neighbor_set (⇑f v) ↔ w ∈ G.neighbor_set v

source

@[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)) :

⇑(f.map_edge_set) e = ↑f.map_edge_set e

source

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') :

↥(G.edge_set) ↪ ↥(G'.edge_set)

A graph embedding induces an embedding of edge sets.

Equations

f.map_edge_set = {to_fun := ↑f.map_edge_set, inj' := _}

source

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) :

↥(G.neighbor_set v) ↪ ↥(G'.neighbor_set (⇑f v))

A graph embedding induces an embedding of neighbor sets.

Equations

f.map_neighbor_set v = {to_fun := λ (w : ↥(G.neighbor_set v)), ⟨⇑f ↑w, _⟩, inj' := _}

source

@[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)) :

↑(⇑(f.map_neighbor_set v) w) = ⇑f ↑w

source

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.

source

@[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

source

def simple_graph.iso.refl {V : Type u} {G : simple_graph V} :

G ≃g G

The identity isomorphism of a graph with itself.

source

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.

source

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.

source

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

source

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

source

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} :

sym2.map ⇑f e ∈ G'.edge_set ↔ e ∈ G.edge_set

source

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} :

⇑f w ∈ G'.neighbor_set (⇑f v) ↔ w ∈ G.neighbor_set v

source

@[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)) :

⇑(f.map_edge_set) e = ↑f.map_edge_set e

source

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') :

↥(G.edge_set) ≃ ↥(G'.edge_set)

An isomorphism of graphs induces an equivalence of edge sets.

Equations

f.map_edge_set = {to_fun := ↑f.map_edge_set, inv_fun := ↑(f.symm).map_edge_set, left_inv := _, right_inv := _}

source

@[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)) :

⇑(f.map_edge_set.symm) e = ↑(f.symm).map_edge_set e

source

@[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))) :

↑(⇑((f.map_neighbor_set v).symm) w) = ⇑(f.symm) ↑w

source

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) :

↥(G.neighbor_set v) ≃ ↥(G'.neighbor_set (⇑f v))

A graph isomorphism induces an equivalence of neighbor sets.

Equations

f.map_neighbor_set v = {to_fun := λ (w : ↥(G.neighbor_set v)), ⟨⇑f ↑w, _⟩, inv_fun := λ (w : ↥(G'.neighbor_set (⇑f v))), ⟨⇑(f.symm) ↑w, _⟩, left_inv := _, right_inv := _}

source

@[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)) :

↑(⇑(f.map_neighbor_set v) w) = ⇑f ↑w

source

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') :

fintype.card V = fintype.card W

source

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.

source

@[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