Graph connectivity #

In a simple graph,

A walk is a finite sequence of adjacent vertices, and can be thought of equally well as a sequence of directed edges.
A trail is a walk whose edges each appear no more than once.
A path is a trail whose vertices appear no more than once.
A cycle is a nonempty trail whose first and last vertices are the same and whose vertices except for the first appear no more than once.

Warning: graph theorists mean something different by "path" than do homotopy theorists. A "walk" in graph theory is a "path" in homotopy theory. Another warning: some graph theorists use "path" and "simple path" for "walk" and "path."

Some definitions and theorems have inspiration from multigraph counterparts in [Cho94].

Main definitions #

simple_graph.walk
simple_graph.is_trail, simple_graph.is_path, and simple_graph.is_cycle.
simple_graph.path

Tags #

walks, trails, paths, circuits, cycles

source

inductive simple_graph.walk {V : Type u} (G : simple_graph V) :

V → V → Type u

nil : Π {V : Type u} {G : simple_graph V} {u : V}, G.walk u u
cons : Π {V : Type u} {G : simple_graph V} {u v w : V}, G.adj u v → G.walk v w → G.walk u w

A walk is a sequence of adjacent vertices. For vertices u v : V, the type walk u v consists of all walks starting at u and ending at v.

We say that a walk visits the vertices it contains. The set of vertices a walk visits is simple_graph.walk.support.

source

@[protected, instance]

def simple_graph.walk.decidable_eq {V : Type u} [a : decidable_eq V] (G : simple_graph V) (ᾰ ᾰ_1 : V) :

decidable_eq (G.walk ᾰ ᾰ_1)

source

@[protected, instance]

def simple_graph.walk.inhabited {V : Type u} (G : simple_graph V) (v : V) :

inhabited (G.walk v v)

Equations

simple_graph.walk.inhabited G v = {default := simple_graph.walk.nil v}

source

theorem simple_graph.walk.exists_eq_cons_of_ne {V : Type u} {G : simple_graph V} {u v : V} (hne : u ≠ v) (p : G.walk u v) :

∃ (w : V) (h : G.adj u w) (p' : G.walk w v), p = simple_graph.walk.cons h p'

source

def simple_graph.walk.length {V : Type u} {G : simple_graph V} {u v : V} :

G.walk u v → ℕ

The length of a walk is the number of edges along it.

Equations

(simple_graph.walk.cons _x_2 q).length = q.length.succ
simple_graph.walk.nil.length = 0

source

def simple_graph.walk.append {V : Type u} {G : simple_graph V} {u v w : V} :

G.walk u v → G.walk v w → G.walk u w

The concatenation of two compatible walks.

Equations

(simple_graph.walk.cons h p).append q = simple_graph.walk.cons h (p.append q)
simple_graph.walk.nil.append q = q

source

@[protected]

def simple_graph.walk.reverse_aux {V : Type u} {G : simple_graph V} {u v w : V} :

G.walk u v → G.walk u w → G.walk v w

The concatenation of the reverse of the first walk with the second walk.

Equations

(simple_graph.walk.cons h p).reverse_aux q = p.reverse_aux (simple_graph.walk.cons _ q)
simple_graph.walk.nil.reverse_aux q = q

source

def simple_graph.walk.reverse {V : Type u} {G : simple_graph V} {u v : V} (w : G.walk u v) :

G.walk v u

The walk in reverse.

Equations

w.reverse = w.reverse_aux simple_graph.walk.nil

source

def simple_graph.walk.get_vert {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) (n : ℕ) :

Get the nth vertex from a walk, where n is generally expected to be between 0 and p.length, inclusive. If n is greater than or equal to p.length, the result is the path's endpoint.

Equations

(simple_graph.walk.cons _x q).get_vert (n + 1) = q.get_vert n
(simple_graph.walk.cons _x _x_1).get_vert 0 = u
simple_graph.walk.nil.get_vert _x = u

source

@[simp]

theorem simple_graph.walk.cons_append {V : Type u} {G : simple_graph V} {u v w x : V} (h : G.adj u v) (p : G.walk v w) (q : G.walk w x) :

(simple_graph.walk.cons h p).append q = simple_graph.walk.cons h (p.append q)

source

@[simp]

theorem simple_graph.walk.cons_nil_append {V : Type u} {G : simple_graph V} {u v w : V} (h : G.adj u v) (p : G.walk v w) :

(simple_graph.walk.cons h simple_graph.walk.nil).append p = simple_graph.walk.cons h p

source

@[simp]

theorem simple_graph.walk.append_nil {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :

p.append simple_graph.walk.nil = p

source

@[simp]

theorem simple_graph.walk.nil_append {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :

simple_graph.walk.nil.append p = p

source

theorem simple_graph.walk.append_assoc {V : Type u} {G : simple_graph V} {u v w x : V} (p : G.walk u v) (q : G.walk v w) (r : G.walk w x) :

p.append (q.append r) = (p.append q).append r

source

@[simp]

theorem simple_graph.walk.reverse_nil {V : Type u} {G : simple_graph V} {u : V} :

simple_graph.walk.nil.reverse = simple_graph.walk.nil

source

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

(simple_graph.walk.cons h simple_graph.walk.nil).reverse = simple_graph.walk.cons _ simple_graph.walk.nil

source

@[simp]

theorem simple_graph.walk.cons_reverse_aux {V : Type u} {G : simple_graph V} {u v w x : V} (p : G.walk u v) (q : G.walk w x) (h : G.adj w u) :

(simple_graph.walk.cons h p).reverse_aux q = p.reverse_aux (simple_graph.walk.cons _ q)

source

@[protected, simp]

theorem simple_graph.walk.append_reverse_aux {V : Type u} {G : simple_graph V} {u v w x : V} (p : G.walk u v) (q : G.walk v w) (r : G.walk u x) :

(p.append q).reverse_aux r = q.reverse_aux (p.reverse_aux r)

source

@[protected, simp]

theorem simple_graph.walk.reverse_aux_append {V : Type u} {G : simple_graph V} {u v w x : V} (p : G.walk u v) (q : G.walk u w) (r : G.walk w x) :

(p.reverse_aux q).append r = p.reverse_aux (q.append r)

source

@[protected]

theorem simple_graph.walk.reverse_aux_eq_reverse_append {V : Type u} {G : simple_graph V} {u v w : V} (p : G.walk u v) (q : G.walk u w) :

p.reverse_aux q = p.reverse.append q

source

@[simp]

theorem simple_graph.walk.reverse_cons {V : Type u} {G : simple_graph V} {u v w : V} (h : G.adj u v) (p : G.walk v w) :

(simple_graph.walk.cons h p).reverse = p.reverse.append (simple_graph.walk.cons _ simple_graph.walk.nil)

source

@[simp]

theorem simple_graph.walk.reverse_append {V : Type u} {G : simple_graph V} {u v w : V} (p : G.walk u v) (q : G.walk v w) :

(p.append q).reverse = q.reverse.append p.reverse

source

@[simp]

theorem simple_graph.walk.reverse_reverse {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :

p.reverse.reverse = p

source

@[simp]

theorem simple_graph.walk.length_nil {V : Type u} {G : simple_graph V} {u : V} :

simple_graph.walk.nil.length = 0

source

@[simp]

theorem simple_graph.walk.length_cons {V : Type u} {G : simple_graph V} {u v w : V} (h : G.adj u v) (p : G.walk v w) :

(simple_graph.walk.cons h p).length = p.length + 1

source

@[simp]

theorem simple_graph.walk.length_append {V : Type u} {G : simple_graph V} {u v w : V} (p : G.walk u v) (q : G.walk v w) :

(p.append q).length = p.length + q.length

source

@[protected, simp]

theorem simple_graph.walk.length_reverse_aux {V : Type u} {G : simple_graph V} {u v w : V} (p : G.walk u v) (q : G.walk u w) :

(p.reverse_aux q).length = p.length + q.length

source

@[simp]

theorem simple_graph.walk.length_reverse {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :

p.reverse.length = p.length

source

def simple_graph.walk.support {V : Type u} {G : simple_graph V} {u v : V} :

G.walk u v → list V

The support of a walk is the list of vertices it visits in order.

Equations

(simple_graph.walk.cons h p).support = u :: p.support
simple_graph.walk.nil.support = [u]

source

def simple_graph.walk.edges {V : Type u} {G : simple_graph V} {u v : V} :

G.walk u v → list (sym2 V)

The edges of a walk is the list of edges it visits in order.

Equations

(simple_graph.walk.cons h p).edges = ⟦(u, x)⟧ :: p.edges
simple_graph.walk.nil.edges = list.nil

source

@[simp]

theorem simple_graph.walk.support_nil {V : Type u} {G : simple_graph V} {u : V} :

simple_graph.walk.nil.support = [u]

source

@[simp]

theorem simple_graph.walk.support_cons {V : Type u} {G : simple_graph V} {u v w : V} (h : G.adj u v) (p : G.walk v w) :

(simple_graph.walk.cons h p).support = u :: p.support

source

theorem simple_graph.walk.support_append {V : Type u} {G : simple_graph V} {u v w : V} (p : G.walk u v) (p' : G.walk v w) :

(p.append p').support = p.support ++ p'.support.tail

source

@[simp]

theorem simple_graph.walk.support_reverse {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :

p.reverse.support = p.support.reverse

source

theorem simple_graph.walk.support_ne_nil {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :

p.support ≠ list.nil

source

theorem simple_graph.walk.tail_support_append {V : Type u} {G : simple_graph V} {u v w : V} (p : G.walk u v) (p' : G.walk v w) :

(p.append p').support.tail = p.support.tail ++ p'.support.tail

source

theorem simple_graph.walk.support_eq_cons {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :

p.support = u :: p.support.tail

source

@[simp]

theorem simple_graph.walk.start_mem_support {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :

u ∈ p.support

source

@[simp]

theorem simple_graph.walk.end_mem_support {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :

v ∈ p.support

source

theorem simple_graph.walk.mem_support_iff {V : Type u} {G : simple_graph V} {u v w : V} (p : G.walk u v) :

w ∈ p.support ↔ w = u ∨ w ∈ p.support.tail

source

@[simp]

theorem simple_graph.walk.mem_tail_support_append_iff {V : Type u} {G : simple_graph V} {t u v w : V} (p : G.walk u v) (p' : G.walk v w) :

t ∈ (p.append p').support.tail ↔ t ∈ p.support.tail ∨ t ∈ p'.support.tail

source

@[simp]

theorem simple_graph.walk.end_mem_tail_support_of_ne {V : Type u} {G : simple_graph V} {u v : V} (h : u ≠ v) (p : G.walk u v) :

v ∈ p.support.tail

source

@[simp]

theorem simple_graph.walk.mem_support_append_iff {V : Type u} {G : simple_graph V} {t u v w : V} (p : G.walk u v) (p' : G.walk v w) :

t ∈ (p.append p').support ↔ t ∈ p.support ∨ t ∈ p'.support

source

theorem simple_graph.walk.coe_support {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :

↑(p.support) = {u} + ↑(p.support.tail)

source

theorem simple_graph.walk.coe_support_append {V : Type u} {G : simple_graph V} {u v w : V} (p : G.walk u v) (p' : G.walk v w) :

↑((p.append p').support) = {u} + ↑(p.support.tail) + ↑(p'.support.tail)

source

theorem simple_graph.walk.coe_support_append' {V : Type u} {G : simple_graph V} [decidable_eq V] {u v w : V} (p : G.walk u v) (p' : G.walk v w) :

↑((p.append p').support) = ↑(p.support) + ↑(p'.support) - {v}

source

theorem simple_graph.walk.chain_adj_support_aux {V : Type u} {G : simple_graph V} {u v w : V} (h : G.adj u v) (p : G.walk v w) :

list.chain G.adj u p.support

source

theorem simple_graph.walk.chain_adj_support {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :

list.chain' G.adj p.support

source

theorem simple_graph.walk.edges_subset_edge_set {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) {e : sym2 V} (h : e ∈ p.edges) :

e ∈ G.edge_set

Every edge in a walk's edge list is an edge of the graph. It is written in this form to avoid unsightly coercions.

source

@[simp]

theorem simple_graph.walk.edges_nil {V : Type u} {G : simple_graph V} {u : V} :

simple_graph.walk.nil.edges = list.nil

source

@[simp]

theorem simple_graph.walk.edges_cons {V : Type u} {G : simple_graph V} {u v w : V} (h : G.adj u v) (p : G.walk v w) :

(simple_graph.walk.cons h p).edges = ⟦(u, v)⟧ :: p.edges

source

@[simp]

theorem simple_graph.walk.edges_append {V : Type u} {G : simple_graph V} {u v w : V} (p : G.walk u v) (p' : G.walk v w) :

(p.append p').edges = p.edges ++ p'.edges

source

@[simp]

theorem simple_graph.walk.edges_reverse {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :

p.reverse.edges = p.edges.reverse

source

@[simp]

theorem simple_graph.walk.length_support {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :

p.support.length = p.length + 1

source

@[simp]

theorem simple_graph.walk.length_edges {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :

p.edges.length = p.length

source

theorem simple_graph.walk.mem_support_of_mem_edges {V : Type u} {G : simple_graph V} {t u v w : V} (p : G.walk v w) (he : ⟦(t, u)⟧ ∈ p.edges) :

t ∈ p.support

source

theorem simple_graph.walk.edges_nodup_of_support_nodup {V : Type u} {G : simple_graph V} {u v : V} {p : G.walk u v} (h : p.support.nodup) :

p.edges.nodup

source

structure simple_graph.walk.is_trail {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :

Prop

edges_nodup : p.edges.nodup

A trail is a walk with no repeating edges.

source

structure simple_graph.walk.is_path {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :

Prop

to_trail : p.is_trail
support_nodup : p.support.nodup

A path is a walk with no repeating vertices. Use simple_graph.walk.is_path.mk' for a simpler constructor.

source

structure simple_graph.walk.is_circuit {V : Type u} {G : simple_graph V} {u : V} (p : G.walk u u) :

Prop

to_trail : p.is_trail
ne_nil : p ≠ simple_graph.walk.nil

A circuit at u : V is a nonempty trail beginning and ending at u.

source

structure simple_graph.walk.is_cycle {V : Type u} {G : simple_graph V} [decidable_eq V] {u : V} (p : G.walk u u) :

Prop

to_circuit : p.is_circuit
support_nodup : p.support.tail.nodup

A cycle at u : V is a circuit at u whose only repeating vertex is u (which appears exactly twice).

source

theorem simple_graph.walk.is_trail_def {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :

p.is_trail ↔ p.edges.nodup

source

theorem simple_graph.walk.is_path.mk' {V : Type u} {G : simple_graph V} {u v : V} {p : G.walk u v} (h : p.support.nodup) :

p.is_path

source

theorem simple_graph.walk.is_path_def {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :

p.is_path ↔ p.support.nodup

source

theorem simple_graph.walk.is_cycle_def {V : Type u} {G : simple_graph V} [decidable_eq V] {u : V} (p : G.walk u u) :

p.is_cycle ↔ p.is_trail ∧ p ≠ simple_graph.walk.nil ∧ p.support.tail.nodup

source

@[simp]

theorem simple_graph.walk.is_trail.nil {V : Type u} {G : simple_graph V} {u : V} :

simple_graph.walk.nil.is_trail

source

theorem simple_graph.walk.is_trail.of_cons {V : Type u} {G : simple_graph V} {u v w : V} {h : G.adj u v} {p : G.walk v w} :

(simple_graph.walk.cons h p).is_trail → p.is_trail

source

@[simp]

theorem simple_graph.walk.cons_is_trail_iff {V : Type u} {G : simple_graph V} {u v w : V} (h : G.adj u v) (p : G.walk v w) :

(simple_graph.walk.cons h p).is_trail ↔ p.is_trail ∧ ⟦(u, v)⟧ ∉ p.edges

source

theorem simple_graph.walk.is_trail.reverse {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) (h : p.is_trail) :

p.reverse.is_trail

source

@[simp]

theorem simple_graph.walk.reverse_is_trail_iff {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :

p.reverse.is_trail ↔ p.is_trail

source

theorem simple_graph.walk.is_trail.of_append_left {V : Type u} {G : simple_graph V} {u v w : V} {p : G.walk u v} {q : G.walk v w} (h : (p.append q).is_trail) :

p.is_trail

source

theorem simple_graph.walk.is_trail.of_append_right {V : Type u} {G : simple_graph V} {u v w : V} {p : G.walk u v} {q : G.walk v w} (h : (p.append q).is_trail) :

q.is_trail

source

theorem simple_graph.walk.is_trail.count_edges_le_one {V : Type u} {G : simple_graph V} [decidable_eq V] {u v : V} {p : G.walk u v} (h : p.is_trail) (e : sym2 V) :

list.count e p.edges ≤ 1

source

theorem simple_graph.walk.is_trail.count_edges_eq_one {V : Type u} {G : simple_graph V} [decidable_eq V] {u v : V} {p : G.walk u v} (h : p.is_trail) {e : sym2 V} (he : e ∈ p.edges) :

list.count e p.edges = 1

source

@[simp]

theorem simple_graph.walk.is_path.nil {V : Type u} {G : simple_graph V} {u : V} :

simple_graph.walk.nil.is_path

source

theorem simple_graph.walk.is_path.of_cons {V : Type u} {G : simple_graph V} {u v w : V} {h : G.adj u v} {p : G.walk v w} :

(simple_graph.walk.cons h p).is_path → p.is_path

source

@[simp]

theorem simple_graph.walk.cons_is_path_iff {V : Type u} {G : simple_graph V} {u v w : V} (h : G.adj u v) (p : G.walk v w) :

(simple_graph.walk.cons h p).is_path ↔ p.is_path ∧ u ∉ p.support

source

theorem simple_graph.walk.is_path.reverse {V : Type u} {G : simple_graph V} {u v : V} {p : G.walk u v} (h : p.is_path) :

p.reverse.is_path

source

@[simp]

theorem simple_graph.walk.is_path_reverse_iff {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :

p.reverse.is_path ↔ p.is_path

source

theorem simple_graph.walk.is_path.of_append_left {V : Type u} {G : simple_graph V} {u v w : V} {p : G.walk u v} {q : G.walk v w} :

(p.append q).is_path → p.is_path

source

theorem simple_graph.walk.is_path.of_append_right {V : Type u} {G : simple_graph V} {u v w : V} {p : G.walk u v} {q : G.walk v w} (h : (p.append q).is_path) :

q.is_path