# 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 [Chou1994].

## Main definitions #

• SimpleGraph.Walk (with accompanying pattern definitions SimpleGraph.Walk.nil' and SimpleGraph.Walk.cons')

• SimpleGraph.Walk.IsTrail, SimpleGraph.Walk.IsPath, and SimpleGraph.Walk.IsCycle.

• SimpleGraph.Path

• SimpleGraph.Walk.map and SimpleGraph.Path.map for the induced map on walks, given an (injective) graph homomorphism.

• SimpleGraph.Reachable for the relation of whether there exists a walk between a given pair of vertices

• SimpleGraph.Preconnected and SimpleGraph.Connected are predicates on simple graphs for whether every vertex can be reached from every other, and in the latter case, whether the vertex type is nonempty.

• SimpleGraph.ConnectedComponent is the type of connected components of a given graph.

• SimpleGraph.IsBridge for whether an edge is a bridge edge

## Main statements #

• SimpleGraph.isBridge_iff_mem_and_forall_cycle_not_mem characterizes bridge edges in terms of there being no cycle containing them.

## Tags #

walks, trails, paths, circuits, cycles, bridge edges

inductive SimpleGraph.Walk {V : Type u} (G : ) :
VVType u

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 SimpleGraph.Walk.support.

See SimpleGraph.Walk.nil' and SimpleGraph.Walk.cons' for patterns that can be useful in definitions since they make the vertices explicit.

• nil: {V : Type u} → {G : } → {u : V} → G.Walk u u
• cons: {V : Type u} → {G : } → {u v w : V} → G.Adj u vG.Walk v wG.Walk u w
Instances For
instance SimpleGraph.instDecidableEqWalk :
{V : Type u_1} → {G : } → {a a_1 : V} → [inst : ] → DecidableEq (G.Walk a a_1)
Equations
• SimpleGraph.instDecidableEqWalk = SimpleGraph.decEqWalk✝
@[simp]
theorem SimpleGraph.Walk.instInhabited_default {V : Type u} (G : ) (v : V) :
default = SimpleGraph.Walk.nil
instance SimpleGraph.Walk.instInhabited {V : Type u} (G : ) (v : V) :
Inhabited (G.Walk v v)
Equations
• = { default := SimpleGraph.Walk.nil }
@[reducible, match_pattern]
def SimpleGraph.Adj.toWalk {V : Type u} {G : } {u : V} {v : V} (h : G.Adj u v) :
G.Walk u v

The one-edge walk associated to a pair of adjacent vertices.

Equations
Instances For
@[reducible, match_pattern, inline]
abbrev SimpleGraph.Walk.nil' {V : Type u} {G : } (u : V) :
G.Walk u u

Pattern to get Walk.nil with the vertex as an explicit argument.

Equations
• = SimpleGraph.Walk.nil
Instances For
@[reducible, match_pattern, inline]
abbrev SimpleGraph.Walk.cons' {V : Type u} {G : } (u : V) (v : V) (w : V) (h : G.Adj u v) (p : G.Walk v w) :
G.Walk u w

Pattern to get Walk.cons with the vertices as explicit arguments.

Equations
Instances For
def SimpleGraph.Walk.copy {V : Type u} {G : } {u : V} {v : V} {u' : V} {v' : V} (p : G.Walk u v) (hu : u = u') (hv : v = v') :
G.Walk u' v'

Change the endpoints of a walk using equalities. This is helpful for relaxing definitional equality constraints and to be able to state otherwise difficult-to-state lemmas. While this is a simple wrapper around Eq.rec, it gives a canonical way to write it.

The simp-normal form is for the copy to be pushed outward. That way calculations can occur within the "copy context."

Equations
• p.copy hu hv = huhvp
Instances For
@[simp]
theorem SimpleGraph.Walk.copy_rfl_rfl {V : Type u} {G : } {u : V} {v : V} (p : G.Walk u v) :
p.copy = p
@[simp]
theorem SimpleGraph.Walk.copy_copy {V : Type u} {G : } {u : V} {v : V} {u' : V} {v' : V} {u'' : V} {v'' : V} (p : G.Walk u v) (hu : u = u') (hv : v = v') (hu' : u' = u'') (hv' : v' = v'') :
(p.copy hu hv).copy hu' hv' = p.copy
@[simp]
theorem SimpleGraph.Walk.copy_nil {V : Type u} {G : } {u : V} {u' : V} (hu : u = u') :
SimpleGraph.Walk.nil.copy hu hu = SimpleGraph.Walk.nil
theorem SimpleGraph.Walk.copy_cons {V : Type u} {G : } {u : V} {v : V} {w : V} {u' : V} {w' : V} (h : G.Adj u v) (p : G.Walk v w) (hu : u = u') (hw : w = w') :
().copy hu hw = SimpleGraph.Walk.cons (p.copy hw)
@[simp]
theorem SimpleGraph.Walk.cons_copy {V : Type u} {G : } {u : V} {v : V} {w : V} {v' : V} {w' : V} (h : G.Adj u v) (p : G.Walk v' w') (hv : v' = v) (hw : w' = w) :
SimpleGraph.Walk.cons h (p.copy hv hw) = ().copy hw
theorem SimpleGraph.Walk.exists_eq_cons_of_ne {V : Type u} {G : } {u : V} {v : V} (hne : u v) (p : G.Walk u v) :
∃ (w : V) (h : G.Adj u w) (p' : G.Walk w v), p =
def SimpleGraph.Walk.length {V : Type u} {G : } {u : V} {v : V} :
G.Walk u v

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

Equations
• SimpleGraph.Walk.nil.length = 0
• ().length = q.length.succ
Instances For
def SimpleGraph.Walk.append {V : Type u} {G : } {u : V} {v : V} {w : V} :
G.Walk u vG.Walk v wG.Walk u w

The concatenation of two compatible walks.

Equations
Instances For
def SimpleGraph.Walk.concat {V : Type u} {G : } {u : V} {v : V} {w : V} (p : G.Walk u v) (h : G.Adj v w) :
G.Walk u w

The reversed version of SimpleGraph.Walk.cons, concatenating an edge to the end of a walk.

Equations
Instances For
theorem SimpleGraph.Walk.concat_eq_append {V : Type u} {G : } {u : V} {v : V} {w : V} (p : G.Walk u v) (h : G.Adj v w) :
p.concat h = p.append (SimpleGraph.Walk.cons h SimpleGraph.Walk.nil)
def SimpleGraph.Walk.reverseAux {V : Type u} {G : } {u : V} {v : V} {w : V} :
G.Walk u vG.Walk u wG.Walk v w

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

Equations
• SimpleGraph.Walk.nil.reverseAux x = x
• ().reverseAux x = p.reverseAux ()
Instances For
def SimpleGraph.Walk.reverse {V : Type u} {G : } {u : V} {v : V} (w : G.Walk u v) :
G.Walk v u

The walk in reverse.

Equations
• w.reverse = w.reverseAux SimpleGraph.Walk.nil
Instances For
def SimpleGraph.Walk.getVert {V : Type u} {G : } {u : V} {v : V} :
G.Walk u vV

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
• SimpleGraph.Walk.nil.getVert x = u
• ().getVert 0 = u
• ().getVert n.succ = q.getVert n
Instances For
@[simp]
theorem SimpleGraph.Walk.getVert_zero {V : Type u} {G : } {u : V} {v : V} (w : G.Walk u v) :
w.getVert 0 = u
theorem SimpleGraph.Walk.getVert_of_length_le {V : Type u} {G : } {u : V} {v : V} (w : G.Walk u v) {i : } (hi : w.length i) :
w.getVert i = v
@[simp]
theorem SimpleGraph.Walk.getVert_length {V : Type u} {G : } {u : V} {v : V} (w : G.Walk u v) :
w.getVert w.length = v
theorem SimpleGraph.Walk.adj_getVert_succ {V : Type u} {G : } {u : V} {v : V} (w : G.Walk u v) {i : } (hi : i < w.length) :
G.Adj (w.getVert i) (w.getVert (i + 1))
@[simp]
theorem SimpleGraph.Walk.cons_append {V : Type u} {G : } {u : V} {v : V} {w : V} {x : V} (h : G.Adj u v) (p : G.Walk v w) (q : G.Walk w x) :
().append q = SimpleGraph.Walk.cons h (p.append q)
@[simp]
theorem SimpleGraph.Walk.cons_nil_append {V : Type u} {G : } {u : V} {v : V} {w : V} (h : G.Adj u v) (p : G.Walk v w) :
(SimpleGraph.Walk.cons h SimpleGraph.Walk.nil).append p =
@[simp]
theorem SimpleGraph.Walk.append_nil {V : Type u} {G : } {u : V} {v : V} (p : G.Walk u v) :
p.append SimpleGraph.Walk.nil = p
@[simp]
theorem SimpleGraph.Walk.nil_append {V : Type u} {G : } {u : V} {v : V} (p : G.Walk u v) :
SimpleGraph.Walk.nil.append p = p
theorem SimpleGraph.Walk.append_assoc {V : Type u} {G : } {u : V} {v : V} {w : V} {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
@[simp]
theorem SimpleGraph.Walk.append_copy_copy {V : Type u} {G : } {u : V} {v : V} {w : V} {u' : V} {v' : V} {w' : V} (p : G.Walk u v) (q : G.Walk v w) (hu : u = u') (hv : v = v') (hw : w = w') :
(p.copy hu hv).append (q.copy hv hw) = (p.append q).copy hu hw
theorem SimpleGraph.Walk.concat_nil {V : Type u} {G : } {u : V} {v : V} (h : G.Adj u v) :
SimpleGraph.Walk.nil.concat h = SimpleGraph.Walk.cons h SimpleGraph.Walk.nil
@[simp]
theorem SimpleGraph.Walk.concat_cons {V : Type u} {G : } {u : V} {v : V} {w : V} {x : V} (h : G.Adj u v) (p : G.Walk v w) (h' : G.Adj w x) :
().concat h' = SimpleGraph.Walk.cons h (p.concat h')
theorem SimpleGraph.Walk.append_concat {V : Type u} {G : } {u : V} {v : V} {w : V} {x : V} (p : G.Walk u v) (q : G.Walk v w) (h : G.Adj w x) :
p.append (q.concat h) = (p.append q).concat h
theorem SimpleGraph.Walk.concat_append {V : Type u} {G : } {u : V} {v : V} {w : V} {x : V} (p : G.Walk u v) (h : G.Adj v w) (q : G.Walk w x) :
(p.concat h).append q = p.append ()
theorem SimpleGraph.Walk.exists_cons_eq_concat {V : Type u} {G : } {u : V} {v : V} {w : V} (h : G.Adj u v) (p : G.Walk v w) :
∃ (x : V) (q : G.Walk u x) (h' : G.Adj x w), = q.concat h'

A non-trivial cons walk is representable as a concat walk.

theorem SimpleGraph.Walk.exists_concat_eq_cons {V : Type u} {G : } {u : V} {v : V} {w : V} (p : G.Walk u v) (h : G.Adj v w) :
∃ (x : V) (h' : G.Adj u x) (q : G.Walk x w), p.concat h =

A non-trivial concat walk is representable as a cons walk.

@[simp]
theorem SimpleGraph.Walk.reverse_nil {V : Type u} {G : } {u : V} :
SimpleGraph.Walk.nil.reverse = SimpleGraph.Walk.nil
theorem SimpleGraph.Walk.reverse_singleton {V : Type u} {G : } {u : V} {v : V} (h : G.Adj u v) :
(SimpleGraph.Walk.cons h SimpleGraph.Walk.nil).reverse = SimpleGraph.Walk.cons SimpleGraph.Walk.nil
@[simp]
theorem SimpleGraph.Walk.cons_reverseAux {V : Type u} {G : } {u : V} {v : V} {w : V} {x : V} (p : G.Walk u v) (q : G.Walk w x) (h : G.Adj w u) :
().reverseAux q = p.reverseAux ()
@[simp]
theorem SimpleGraph.Walk.append_reverseAux {V : Type u} {G : } {u : V} {v : V} {w : V} {x : V} (p : G.Walk u v) (q : G.Walk v w) (r : G.Walk u x) :
(p.append q).reverseAux r = q.reverseAux (p.reverseAux r)
@[simp]
theorem SimpleGraph.Walk.reverseAux_append {V : Type u} {G : } {u : V} {v : V} {w : V} {x : V} (p : G.Walk u v) (q : G.Walk u w) (r : G.Walk w x) :
(p.reverseAux q).append r = p.reverseAux (q.append r)
theorem SimpleGraph.Walk.reverseAux_eq_reverse_append {V : Type u} {G : } {u : V} {v : V} {w : V} (p : G.Walk u v) (q : G.Walk u w) :
p.reverseAux q = p.reverse.append q
@[simp]
theorem SimpleGraph.Walk.reverse_cons {V : Type u} {G : } {u : V} {v : V} {w : V} (h : G.Adj u v) (p : G.Walk v w) :
().reverse = p.reverse.append (SimpleGraph.Walk.cons SimpleGraph.Walk.nil)
@[simp]
theorem SimpleGraph.Walk.reverse_copy {V : Type u} {G : } {u : V} {v : V} {u' : V} {v' : V} (p : G.Walk u v) (hu : u = u') (hv : v = v') :
(p.copy hu hv).reverse = p.reverse.copy hv hu
@[simp]
theorem SimpleGraph.Walk.reverse_append {V : Type u} {G : } {u : V} {v : V} {w : V} (p : G.Walk u v) (q : G.Walk v w) :
(p.append q).reverse = q.reverse.append p.reverse
@[simp]
theorem SimpleGraph.Walk.reverse_concat {V : Type u} {G : } {u : V} {v : V} {w : V} (p : G.Walk u v) (h : G.Adj v w) :
(p.concat h).reverse = SimpleGraph.Walk.cons p.reverse
@[simp]
theorem SimpleGraph.Walk.reverse_reverse {V : Type u} {G : } {u : V} {v : V} (p : G.Walk u v) :
p.reverse.reverse = p
@[simp]
theorem SimpleGraph.Walk.length_nil {V : Type u} {G : } {u : V} :
SimpleGraph.Walk.nil.length = 0
@[simp]
theorem SimpleGraph.Walk.length_cons {V : Type u} {G : } {u : V} {v : V} {w : V} (h : G.Adj u v) (p : G.Walk v w) :
().length = p.length + 1
@[simp]
theorem SimpleGraph.Walk.length_copy {V : Type u} {G : } {u : V} {v : V} {u' : V} {v' : V} (p : G.Walk u v) (hu : u = u') (hv : v = v') :
(p.copy hu hv).length = p.length
@[simp]
theorem SimpleGraph.Walk.length_append {V : Type u} {G : } {u : V} {v : V} {w : V} (p : G.Walk u v) (q : G.Walk v w) :
(p.append q).length = p.length + q.length
@[simp]
theorem SimpleGraph.Walk.length_concat {V : Type u} {G : } {u : V} {v : V} {w : V} (p : G.Walk u v) (h : G.Adj v w) :
(p.concat h).length = p.length + 1
@[simp]
theorem SimpleGraph.Walk.length_reverseAux {V : Type u} {G : } {u : V} {v : V} {w : V} (p : G.Walk u v) (q : G.Walk u w) :
(p.reverseAux q).length = p.length + q.length
@[simp]
theorem SimpleGraph.Walk.length_reverse {V : Type u} {G : } {u : V} {v : V} (p : G.Walk u v) :
p.reverse.length = p.length
theorem SimpleGraph.Walk.eq_of_length_eq_zero {V : Type u} {G : } {u : V} {v : V} {p : G.Walk u v} :
p.length = 0u = v
theorem SimpleGraph.Walk.adj_of_length_eq_one {V : Type u} {G : } {u : V} {v : V} {p : G.Walk u v} :
p.length = 1G.Adj u v
@[simp]
theorem SimpleGraph.Walk.exists_length_eq_zero_iff {V : Type u} {G : } {u : V} {v : V} :
(∃ (p : G.Walk u v), p.length = 0) u = v
@[simp]
theorem SimpleGraph.Walk.length_eq_zero_iff {V : Type u} {G : } {u : V} {p : G.Walk u u} :
p.length = 0 p = SimpleGraph.Walk.nil
theorem SimpleGraph.Walk.getVert_append {V : Type u} {G : } {u : V} {v : V} {w : V} (p : G.Walk u v) (q : G.Walk v w) (i : ) :
(p.append q).getVert i = if i < p.length then p.getVert i else q.getVert (i - p.length)
theorem SimpleGraph.Walk.getVert_reverse {V : Type u} {G : } {u : V} {v : V} (p : G.Walk u v) (i : ) :
p.reverse.getVert i = p.getVert (p.length - i)
def SimpleGraph.Walk.concatRecAux {V : Type u} {G : } {motive : (u v : V) → G.Walk u vSort u_1} (Hnil : {u : V} → motive u u SimpleGraph.Walk.nil) (Hconcat : {u v w : V} → (p : G.Walk u v) → (h : G.Adj v w) → motive u v pmotive u w (p.concat h)) {u : V} {v : V} (p : G.Walk u v) :
motive v u p.reverse

Auxiliary definition for SimpleGraph.Walk.concatRec

Equations
Instances For
def SimpleGraph.Walk.concatRec {V : Type u} {G : } {motive : (u v : V) → G.Walk u vSort u_1} (Hnil : {u : V} → motive u u SimpleGraph.Walk.nil) (Hconcat : {u v w : V} → (p : G.Walk u v) → (h : G.Adj v w) → motive u v pmotive u w (p.concat h)) {u : V} {v : V} (p : G.Walk u v) :
motive u v p

Recursor on walks by inducting on SimpleGraph.Walk.concat.

This is inducting from the opposite end of the walk compared to SimpleGraph.Walk.rec, which inducts on SimpleGraph.Walk.cons.

Equations
Instances For
@[simp]
theorem SimpleGraph.Walk.concatRec_nil {V : Type u} {G : } {motive : (u v : V) → G.Walk u vSort u_1} (Hnil : {u : V} → motive u u SimpleGraph.Walk.nil) (Hconcat : {u v w : V} → (p : G.Walk u v) → (h : G.Adj v w) → motive u v pmotive u w (p.concat h)) (u : V) :
SimpleGraph.Walk.concatRec Hnil Hconcat SimpleGraph.Walk.nil = Hnil
@[simp]
theorem SimpleGraph.Walk.concatRec_concat {V : Type u} {G : } {motive : (u v : V) → G.Walk u vSort u_1} (Hnil : {u : V} → motive u u SimpleGraph.Walk.nil) (Hconcat : {u v w : V} → (p : G.Walk u v) → (h : G.Adj v w) → motive u v pmotive u w (p.concat h)) {u : V} {v : V} {w : V} (p : G.Walk u v) (h : G.Adj v w) :
SimpleGraph.Walk.concatRec Hnil Hconcat (p.concat h) = Hconcat p h (SimpleGraph.Walk.concatRec Hnil Hconcat p)
theorem SimpleGraph.Walk.concat_ne_nil {V : Type u} {G : } {u : V} {v : V} (p : G.Walk u v) (h : G.Adj v u) :
p.concat h SimpleGraph.Walk.nil
theorem SimpleGraph.Walk.concat_inj {V : Type u} {G : } {u : V} {v : V} {v' : V} {w : V} {p : G.Walk u v} {h : G.Adj v w} {p' : G.Walk u v'} {h' : G.Adj v' w} (he : p.concat h = p'.concat h') :
∃ (hv : v = v'), p.copy hv = p'
def SimpleGraph.Walk.support {V : Type u} {G : } {u : V} {v : V} :
G.Walk u vList V

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

Equations
• SimpleGraph.Walk.nil.support = [u]
• ().support = u :: q.support
Instances For
def SimpleGraph.Walk.darts {V : Type u} {G : } {u : V} {v : V} :
G.Walk u vList G.Dart

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

Equations
• SimpleGraph.Walk.nil.darts = []
• ().darts = { toProd := (u, v_3), adj := h } :: q.darts
Instances For
def SimpleGraph.Walk.edges {V : Type u} {G : } {u : V} {v : V} (p : G.Walk u v) :

The edges of a walk is the list of edges it visits in order. This is defined to be the list of edges underlying SimpleGraph.Walk.darts.

Equations
• p.edges = List.map SimpleGraph.Dart.edge p.darts
Instances For
@[simp]
theorem SimpleGraph.Walk.support_nil {V : Type u} {G : } {u : V} :
SimpleGraph.Walk.nil.support = [u]
@[simp]
theorem SimpleGraph.Walk.support_cons {V : Type u} {G : } {u : V} {v : V} {w : V} (h : G.Adj u v) (p : G.Walk v w) :
().support = u :: p.support
@[simp]
theorem SimpleGraph.Walk.support_concat {V : Type u} {G : } {u : V} {v : V} {w : V} (p : G.Walk u v) (h : G.Adj v w) :
(p.concat h).support = p.support.concat w
@[simp]
theorem SimpleGraph.Walk.support_copy {V : Type u} {G : } {u : V} {v : V} {u' : V} {v' : V} (p : G.Walk u v) (hu : u = u') (hv : v = v') :
(p.copy hu hv).support = p.support
theorem SimpleGraph.Walk.support_append {V : Type u} {G : } {u : V} {v : V} {w : V} (p : G.Walk u v) (p' : G.Walk v w) :
(p.append p').support = p.support ++ p'.support.tail
@[simp]
theorem SimpleGraph.Walk.support_reverse {V : Type u} {G : } {u : V} {v : V} (p : G.Walk u v) :
p.reverse.support = p.support.reverse
@[simp]
theorem SimpleGraph.Walk.support_ne_nil {V : Type u} {G : } {u : V} {v : V} (p : G.Walk u v) :
p.support []
theorem SimpleGraph.Walk.tail_support_append {V : Type u} {G : } {u : V} {v : V} {w : V} (p : G.Walk u v) (p' : G.Walk v w) :
(p.append p').support.tail = p.support.tail ++ p'.support.tail
theorem SimpleGraph.Walk.support_eq_cons {V : Type u} {G : } {u : V} {v : V} (p : G.Walk u v) :
p.support = u :: p.support.tail
@[simp]
theorem SimpleGraph.Walk.start_mem_support {V : Type u} {G : } {u : V} {v : V} (p : G.Walk u v) :
u p.support
@[simp]
theorem SimpleGraph.Walk.end_mem_support {V : Type u} {G : } {u : V} {v : V} (p : G.Walk u v) :
v p.support
@[simp]
theorem SimpleGraph.Walk.support_nonempty {V : Type u} {G : } {u : V} {v : V} (p : G.Walk u v) :
{w : V | w p.support}.Nonempty
theorem SimpleGraph.Walk.mem_support_iff {V : Type u} {G : } {u : V} {v : V} {w : V} (p : G.Walk u v) :
w p.support w = u w p.support.tail
theorem SimpleGraph.Walk.mem_support_nil_iff {V : Type u} {G : } {u : V} {v : V} :
u SimpleGraph.Walk.nil.support u = v
@[simp]
theorem SimpleGraph.Walk.mem_tail_support_append_iff {V : Type u} {G : } {t : V} {u : V} {v : 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
@[simp]
theorem SimpleGraph.Walk.end_mem_tail_support_of_ne {V : Type u} {G : } {u : V} {v : V} (h : u v) (p : G.Walk u v) :
v p.support.tail
@[simp]
theorem SimpleGraph.Walk.mem_support_append_iff {V : Type u} {G : } {t : V} {u : V} {v : V} {w : V} (p : G.Walk u v) (p' : G.Walk v w) :
t (p.append p').support t p.support t p'.support
@[simp]
theorem SimpleGraph.Walk.subset_support_append_left {V : Type u} {G : } {u : V} {v : V} {w : V} (p : G.Walk u v) (q : G.Walk v w) :
p.support (p.append q).support
@[simp]
theorem SimpleGraph.Walk.subset_support_append_right {V : Type u} {G : } {u : V} {v : V} {w : V} (p : G.Walk u v) (q : G.Walk v w) :
q.support (p.append q).support
theorem SimpleGraph.Walk.coe_support {V : Type u} {G : } {u : V} {v : V} (p : G.Walk u v) :
p.support = {u} + p.support.tail
theorem SimpleGraph.Walk.coe_support_append {V : Type u} {G : } {u : V} {v : V} {w : V} (p : G.Walk u v) (p' : G.Walk v w) :
(p.append p').support = {u} + p.support.tail + p'.support.tail
theorem SimpleGraph.Walk.coe_support_append' {V : Type u} {G : } [] {u : V} {v : V} {w : V} (p : G.Walk u v) (p' : G.Walk v w) :
(p.append p').support = p.support + p'.support - {v}
theorem SimpleGraph.Walk.chain_adj_support {V : Type u} {G : } {u : V} {v : V} {w : V} (h : G.Adj u v) (p : G.Walk v w) :
List.Chain G.Adj u p.support
theorem SimpleGraph.Walk.chain'_adj_support {V : Type u} {G : } {u : V} {v : V} (p : G.Walk u v) :
theorem SimpleGraph.Walk.chain_dartAdj_darts {V : Type u} {G : } {d : G.Dart} {v : V} {w : V} (h : d.toProd.2 = v) (p : G.Walk v w) :
List.Chain G.DartAdj d p.darts
theorem SimpleGraph.Walk.chain'_dartAdj_darts {V : Type u} {G : } {u : V} {v : V} (p : G.Walk u v) :
theorem SimpleGraph.Walk.edges_subset_edgeSet {V : Type u} {G : } {u : V} {v : V} (p : G.Walk u v) ⦃e : Sym2 V :
e p.edgese G.edgeSet

Every edge in a walk's edge list is an edge of the graph. It is written in this form (rather than using ⊆) to avoid unsightly coercions.

theorem SimpleGraph.Walk.adj_of_mem_edges {V : Type u} {G : } {u : V} {v : V} {x : V} {y : V} (p : G.Walk u v) (h : s(x, y) p.edges) :
@[simp]
theorem SimpleGraph.Walk.darts_nil {V : Type u} {G : } {u : V} :
SimpleGraph.Walk.nil.darts = []
@[simp]
theorem SimpleGraph.Walk.darts_cons {V : Type u} {G : } {u : V} {v : V} {w : V} (h : G.Adj u v) (p : G.Walk v w) :
().darts = { toProd := (u, v), adj := h } :: p.darts
@[simp]
theorem SimpleGraph.Walk.darts_concat {V : Type u} {G : } {u : V} {v : V} {w : V} (p : G.Walk u v) (h : G.Adj v w) :
(p.concat h).darts = p.darts.concat { toProd := (v, w), adj := h }
@[simp]
theorem SimpleGraph.Walk.darts_copy {V : Type u} {G : } {u : V} {v : V} {u' : V} {v' : V} (p : G.Walk u v) (hu : u = u') (hv : v = v') :
(p.copy hu hv).darts = p.darts
@[simp]
theorem SimpleGraph.Walk.darts_append {V : Type u} {G : } {u : V} {v : V} {w : V} (p : G.Walk u v) (p' : G.Walk v w) :
(p.append p').darts = p.darts ++ p'.darts
@[simp]
theorem SimpleGraph.Walk.darts_reverse {V : Type u} {G : } {u : V} {v : V} (p : G.Walk u v) :
p.reverse.darts = (List.map SimpleGraph.Dart.symm p.darts).reverse
theorem SimpleGraph.Walk.mem_darts_reverse {V : Type u} {G : } {u : V} {v : V} {d : G.Dart} {p : G.Walk u v} :
d p.reverse.darts d.symm p.darts
theorem SimpleGraph.Walk.cons_map_snd_darts {V : Type u} {G : } {u : V} {v : V} (p : G.Walk u v) :
u :: List.map (fun (x : G.Dart) => x.toProd.2) p.darts = p.support
theorem SimpleGraph.Walk.map_snd_darts {V : Type u} {G : } {u : V} {v : V} (p : G.Walk u v) :
List.map (fun (x : G.Dart) => x.toProd.2) p.darts = p.support.tail
theorem SimpleGraph.Walk.map_fst_darts_append {V : Type u} {G : } {u : V} {v : V} (p : G.Walk u v) :
List.map (fun (x : G.Dart) => x.toProd.1) p.darts ++ [v] = p.support
theorem SimpleGraph.Walk.map_fst_darts {V : Type u} {G : } {u : V} {v : V} (p : G.Walk u v) :
List.map (fun (x : G.Dart) => x.toProd.1) p.darts = p.support.dropLast
@[simp]
theorem SimpleGraph.Walk.edges_nil {V : Type u} {G : } {u : V} :
SimpleGraph.Walk.nil.edges = []
@[simp]
theorem SimpleGraph.Walk.edges_cons {V : Type u} {G : } {u : V} {v : V} {w : V} (h : G.Adj u v) (p : G.Walk v w) :
().edges = s(u, v) :: p.edges
@[simp]
theorem SimpleGraph.Walk.edges_concat {V : Type u} {G : } {u : V} {v : V} {w : V} (p : G.Walk u v) (h : G.Adj v w) :
(p.concat h).edges = p.edges.concat s(v, w)
@[simp]
theorem SimpleGraph.Walk.edges_copy {V : Type u} {G : } {u : V} {v : V} {u' : V} {v' : V} (p : G.Walk u v) (hu : u = u') (hv : v = v') :
(p.copy hu hv).edges = p.edges
@[simp]
theorem SimpleGraph.Walk.edges_append {V : Type u} {G : } {u : V} {v : V} {w : V} (p : G.Walk u v) (p' : G.Walk v w) :
(p.append p').edges = p.edges ++ p'.edges
@[simp]
theorem SimpleGraph.Walk.edges_reverse {V : Type u} {G : } {u : V} {v : V} (p : G.Walk u v) :
p.reverse.edges = p.edges.reverse
@[simp]
theorem SimpleGraph.Walk.length_support {V : Type u} {G : } {u : V} {v : V} (p : G.Walk u v) :
p.support.length = p.length + 1
@[simp]
theorem SimpleGraph.Walk.length_darts {V : Type u} {G : } {u : V} {v : V} (p : G.Walk u v) :
p.darts.length = p.length
@[simp]
theorem SimpleGraph.Walk.length_edges {V : Type u} {G : } {u : V} {v : V} (p : G.Walk u v) :
p.edges.length = p.length
theorem SimpleGraph.Walk.dart_fst_mem_support_of_mem_darts {V : Type u} {G : } {u : V} {v : V} (p : G.Walk u v) {d : G.Dart} :
d p.dartsd.toProd.1 p.support
theorem SimpleGraph.Walk.dart_snd_mem_support_of_mem_darts {V : Type u} {G : } {u : V} {v : V} (p : G.Walk u v) {d : G.Dart} (h : d p.darts) :
d.toProd.2 p.support
theorem SimpleGraph.Walk.fst_mem_support_of_mem_edges {V : Type u} {G : } {t : V} {u : V} {v : V} {w : V} (p : G.Walk v w) (he : s(t, u) p.edges) :
t p.support
theorem SimpleGraph.Walk.snd_mem_support_of_mem_edges {V : Type u} {G : } {t : V} {u : V} {v : V} {w : V} (p : G.Walk v w) (he : s(t, u) p.edges) :
u p.support
theorem SimpleGraph.Walk.darts_nodup_of_support_nodup {V : Type u} {G : } {u : V} {v : V} {p : G.Walk u v} (h : p.support.Nodup) :
p.darts.Nodup
theorem SimpleGraph.Walk.edges_nodup_of_support_nodup {V : Type u} {G : } {u : V} {v : V} {p : G.Walk u v} (h : p.support.Nodup) :
p.edges.Nodup
inductive SimpleGraph.Walk.Nil {V : Type u} {G : } {v : V} {w : V} :
G.Walk v wProp

Predicate for the empty walk.

Solves the dependent type problem where p = G.Walk.nil typechecks only if p has defeq endpoints.

• nil: ∀ {V : Type u} {G : } {u : V}, SimpleGraph.Walk.nil.Nil
Instances For
@[simp]
theorem SimpleGraph.Walk.nil_nil {V : Type u} {G : } {u : V} :
SimpleGraph.Walk.nil.Nil
@[simp]
theorem SimpleGraph.Walk.not_nil_cons {V : Type u} {G : } {u : V} {v : V} {w : V} {h : G.Adj u v} {p : G.Walk v w} :
¬().Nil
instance SimpleGraph.Walk.instDecidableNil {V : Type u} {G : } {v : V} {w : V} (p : G.Walk v w) :
Decidable p.Nil
Equations
• p.instDecidableNil = match w, p with | .(v), SimpleGraph.Walk.nil => | w, =>
theorem SimpleGraph.Walk.Nil.eq {V : Type u} {G : } {v : V} {w : V} {p : G.Walk v w} :
p.Nilv = w
theorem SimpleGraph.Walk.not_nil_of_ne {V : Type u} {G : } {v : V} {w : V} {p : G.Walk v w} :
v w¬p.Nil
theorem SimpleGraph.Walk.nil_iff_support_eq {V : Type u} {G : } {v : V} {w : V} {p : G.Walk v w} :
p.Nil p.support = [v]
theorem SimpleGraph.Walk.nil_iff_length_eq {V : Type u} {G : } {v : V} {w : V} {p : G.Walk v w} :
p.Nil p.length = 0
theorem SimpleGraph.Walk.not_nil_iff {V : Type u} {G : } {v : V} {w : V} {p : G.Walk v w} :
¬p.Nil ∃ (u : V) (h : G.Adj v u) (q : G.Walk u w),
theorem SimpleGraph.Walk.nil_iff_eq_nil {V : Type u} {G : } {v : V} {p : G.Walk v v} :
p.Nil p = SimpleGraph.Walk.nil

A walk with its endpoints defeq is Nil if and only if it is equal to nil.

theorem SimpleGraph.Walk.Nil.eq_nil {V : Type u} {G : } {v : V} {p : G.Walk v v} :
p.Nilp = SimpleGraph.Walk.nil

Alias of the forward direction of SimpleGraph.Walk.nil_iff_eq_nil.

A walk with its endpoints defeq is Nil if and only if it is equal to nil.

def SimpleGraph.Walk.notNilRec {V : Type u} {G : } {u : V} {w : V} {motive : {u w : V} → (p : G.Walk u w) → ¬p.NilSort u_1} (cons : {u v w : V} → (h : G.Adj u v) → (q : G.Walk v w) → motive () ) (p : G.Walk u w) (hp : ¬p.Nil) :
motive p hp
Equations
• One or more equations did not get rendered due to their size.
Instances For
def SimpleGraph.Walk.sndOfNotNil {V : Type u} {G : } {v : V} {w : V} (p : G.Walk v w) (hp : ¬p.Nil) :
V

The second vertex along a non-nil walk.

Equations
Instances For
@[simp]
theorem SimpleGraph.Walk.adj_sndOfNotNil {V : Type u} {G : } {v : V} {w : V} {p : G.Walk v w} (hp : ¬p.Nil) :
G.Adj v (p.sndOfNotNil hp)
def SimpleGraph.Walk.tail {V : Type u} {G : } {u : V} {v : V} (p : G.Walk u v) (hp : ¬p.Nil) :
G.Walk (p.sndOfNotNil hp) v

The walk obtained by removing the first dart of a non-nil walk.

Equations
Instances For
@[simp]
theorem SimpleGraph.Walk.firstDart_toProd {V : Type u} {G : } {v : V} {w : V} (p : G.Walk v w) (hp : ¬p.Nil) :
(p.firstDart hp).toProd = (v, p.sndOfNotNil hp)
def SimpleGraph.Walk.firstDart {V : Type u} {G : } {v : V} {w : V} (p : G.Walk v w) (hp : ¬p.Nil) :
G.Dart

The first dart of a walk.

Equations
• p.firstDart hp = { toProd := (v, p.sndOfNotNil hp), adj := }
Instances For
theorem SimpleGraph.Walk.edge_firstDart {V : Type u} {G : } {v : V} {w : V} (p : G.Walk v w) (hp : ¬p.Nil) :
(p.firstDart hp).edge = s(v, p.sndOfNotNil hp)
@[simp]
theorem SimpleGraph.Walk.cons_tail_eq {V : Type u} {G : } {x : V} {y : V} (p : G.Walk x y) (hp : ¬p.Nil) :
SimpleGraph.Walk.cons (p.tail hp) = p
@[simp]
theorem SimpleGraph.Walk.cons_support_tail {V : Type u} {G : } {x : V} {y : V} (p : G.Walk x y) (hp : ¬p.Nil) :
x :: (p.tail hp).support = p.support
@[simp]
theorem SimpleGraph.Walk.length_tail_add_one {V : Type u} {G : } {x : V} {y : V} {p : G.Walk x y} (hp : ¬p.Nil) :
(p.tail hp).length + 1 = p.length
@[simp]
theorem SimpleGraph.Walk.nil_copy {V : Type u} {G : } {x : V} {y : V} {x' : V} {y' : V} {p : G.Walk x y} (hx : x = x') (hy : y = y') :
(p.copy hx hy).Nil = p.Nil
@[simp]
theorem SimpleGraph.Walk.support_tail {V : Type u} {G : } {v : V} (p : G.Walk v v) (hp : ¬p.Nil) :
(p.tail hp).support = p.support.tail

### Trails, paths, circuits, cycles #

theorem SimpleGraph.Walk.isTrail_def {V : Type u} {G : } {u : V} {v : V} (p : G.Walk u v) :
p.IsTrail p.edges.Nodup
structure SimpleGraph.Walk.IsTrail {V : Type u} {G : } {u : V} {v : V} (p : G.Walk u v) :

A trail is a walk with no repeating edges.

• edges_nodup : p.edges.Nodup
Instances For
theorem SimpleGraph.Walk.IsTrail.edges_nodup {V : Type u} {G : } {u : V} {v : V} {p : G.Walk u v} (self : p.IsTrail) :
p.edges.Nodup
structure SimpleGraph.Walk.IsPath {V : Type u} {G : } {u : V} {v : V} (p : G.Walk u v) extends :

A path is a walk with no repeating vertices. Use SimpleGraph.Walk.IsPath.mk' for a simpler constructor.

• edges_nodup : p.edges.Nodup
• support_nodup : p.support.Nodup
Instances For
theorem SimpleGraph.Walk.IsPath.support_nodup {V : Type u} {G : } {u : V} {v : V} {p : G.Walk u v} (self : p.IsPath) :
p.support.Nodup
theorem SimpleGraph.Walk.IsPath.isTrail {V : Type u} {G : } {u : V} {v : V} {p : G.Walk u v} (h : p.IsPath) :
p.IsTrail
theorem SimpleGraph.Walk.isCircuit_def {V : Type u} {G : } {u : V} (p : G.Walk u u) :
p.IsCircuit p.IsTrail p SimpleGraph.Walk.nil
structure SimpleGraph.Walk.IsCircuit {V : Type u} {G : } {u : V} (p : G.Walk u u) extends :

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

• edges_nodup : p.edges.Nodup
• ne_nil : p SimpleGraph.Walk.nil
Instances For
theorem SimpleGraph.Walk.IsCircuit.ne_nil {V : Type u} {G : } {u : V} {p : G.Walk u u} (self : p.IsCircuit) :
p SimpleGraph.Walk.nil
theorem SimpleGraph.Walk.IsCircuit.isTrail {V : Type u} {G : } {u : V} {p : G.Walk u u} (h : p.IsCircuit) :
p.IsTrail
structure SimpleGraph.Walk.IsCycle {V : Type u} {G : } {u : V} (p : G.Walk u u) extends :

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

• edges_nodup : p.edges.Nodup
• ne_nil : p SimpleGraph.Walk.nil
• support_nodup : p.support.tail.Nodup
Instances For
theorem SimpleGraph.Walk.IsCycle.support_nodup {V : Type u} {G : } {u : V} {p : G.Walk u u} (self : p.IsCycle) :
p.support.tail.Nodup
theorem SimpleGraph.Walk.IsCycle.isCircuit {V : Type u} {G : } {u : V} {p : G.Walk u u} (h : p.IsCycle) :
p.IsCircuit
@[simp]
theorem SimpleGraph.Walk.isTrail_copy {V : Type u} {G : } {u : V} {v : V} {u' : V} {v' : V} (p : G.Walk u v) (hu : u = u') (hv : v = v') :
(p.copy hu hv).IsTrail p.IsTrail
theorem SimpleGraph.Walk.IsPath.mk' {V : Type u} {G : } {u : V} {v : V} {p : G.Walk u v} (h : p.support.Nodup) :
p.IsPath
theorem SimpleGraph.Walk.isPath_def {V : Type u} {G : } {u : V} {v : V} (p : G.Walk u v) :
p.IsPath p.support.Nodup
@[simp]
theorem SimpleGraph.Walk.isPath_copy {V : Type u} {G : } {u : V} {v : V} {u' : V} {v' : V} (p : G.Walk u v) (hu : u = u') (hv : v = v') :
(p.copy hu hv).IsPath p.IsPath
@[simp]
theorem SimpleGraph.Walk.isCircuit_copy {V : Type u} {G : } {u : V} {u' : V} (p : G.Walk u u) (hu : u = u') :
(p.copy hu hu).IsCircuit p.IsCircuit
theorem SimpleGraph.Walk.IsCircuit.not_nil {V : Type u} {G : } {v : V} {p : G.Walk v v} (hp : p.IsCircuit) :
¬p.Nil
theorem SimpleGraph.Walk.isCycle_def {V : Type u} {G : } {u : V} (p : G.Walk u u) :
p.IsCycle p.IsTrail p SimpleGraph.Walk.nil p.support.tail.Nodup
@[simp]
theorem SimpleGraph.Walk.isCycle_copy {V : Type u} {G : } {u : V} {u' : V} (p : G.Walk u u) (hu : u = u') :
(p.copy hu hu).IsCycle p.IsCycle
theorem SimpleGraph.Walk.IsCycle.not_nil {V : Type u} {G : } {v : V} {p : G.Walk v v} (hp : p.IsCycle) :
¬p.Nil
@[simp]
theorem SimpleGraph.Walk.IsTrail.nil {V : Type u} {G : } {u : V} :
SimpleGraph.Walk.nil.IsTrail
theorem SimpleGraph.Walk.IsTrail.of_cons {V : Type u} {G : } {u : V} {v : V} {w : V} {h : G.Adj u v} {p : G.Walk v w} :
().IsTrailp.IsTrail
@[simp]
theorem SimpleGraph.Walk.cons_isTrail_iff {V : Type u} {G : } {u : V} {v : V} {w : V} (h : G.Adj u v) (p : G.Walk v w) :
().IsTrail p.IsTrail s(u, v)p.edges
theorem SimpleGraph.Walk.IsTrail.reverse {V : Type u} {G : } {u : V} {v : V} (p : G.Walk u v) (h : p.IsTrail) :
p.reverse.IsTrail
@[simp]
theorem SimpleGraph.Walk.reverse_isTrail_iff {V : Type u} {G : } {u : V} {v : V} (p : G.Walk u v) :
p.reverse.IsTrail p.IsTrail
theorem SimpleGraph.Walk.IsTrail.of_append_left {V : Type u} {G : } {u : V} {v : V} {w : V} {p : G.Walk u v} {q : G.Walk v w} (h : (p.append q).IsTrail) :
p.IsTrail
theorem SimpleGraph.Walk.IsTrail.of_append_right {V : Type u} {G : } {u : V} {v : V} {w : V} {p : G.Walk u v} {q : G.Walk v w} (h : (p.append q).IsTrail) :
q.IsTrail
theorem SimpleGraph.Walk.IsTrail.count_edges_le_one {V : Type u} {G : } [] {u : V} {v : V} {p : G.Walk u v} (h : p.IsTrail) (e : Sym2 V) :
List.count e p.edges 1
theorem SimpleGraph.Walk.IsTrail.count_edges_eq_one {V : Type u} {G : } [] {u : V} {v : V} {p : G.Walk u v} (h : p.IsTrail) {e : Sym2 V} (he : e p.edges) :
List.count e p.edges = 1
theorem SimpleGraph.Walk.IsPath.nil {V : Type u} {G : } {u : V} :
SimpleGraph.Walk.nil.IsPath
theorem SimpleGraph.Walk.IsPath.of_cons {V : Type u} {G : } {u : V} {v : V} {w : V} {h : G.Adj u v} {p : G.Walk v w} :
().IsPathp.IsPath
@[simp]
theorem SimpleGraph.Walk.cons_isPath_iff {V : Type u} {G : } {u : V} {v : V} {w : V} (h : G.Adj u v) (p : G.Walk v w) :
().IsPath p.IsPath up.support
theorem SimpleGraph.Walk.IsPath.cons {V : Type u} {G : } {u : V} {v : V} {w : V} {p : G.Walk v w} (hp : p.IsPath) (hu : up.support) {h : G.Adj u v} :
().IsPath
@[simp]
theorem SimpleGraph.Walk.isPath_iff_eq_nil {V : Type u} {G : } {u : V} (p : G.Walk u u) :
p.IsPath p = SimpleGraph.Walk.nil
theorem SimpleGraph.Walk.IsPath.reverse {V : Type u} {G : } {u : V} {v : V} {p : G.Walk u v} (h : p.IsPath) :
p.reverse.IsPath
@[simp]
theorem SimpleGraph.Walk.isPath_reverse_iff {V : Type u} {G : } {u : V} {v : V} (p : G.Walk u v) :
p.reverse.IsPath p.IsPath
theorem SimpleGraph.Walk.IsPath.of_append_left {V : Type u} {G : } {u : V} {v : V} {w : V} {p : G.Walk u v} {q : G.Walk v w} :
(p.append q).IsPathp.IsPath
theorem SimpleGraph.Walk.IsPath.of_append_right {V : Type u} {G : } {u : V} {v : V} {w : V} {p : G.Walk u v} {q : G.Walk v w} (h : (p.append q).IsPath) :
q.IsPath
@[simp]
theorem SimpleGraph.Walk.IsCycle.not_of_nil {V : Type u} {G : } {u : V} :
¬SimpleGraph.Walk.nil.IsCycle
theorem SimpleGraph.Walk.IsCycle.ne_bot {V : Type u} {G : } {u : V} {p : G.Walk u u} :
p.IsCycleG
theorem SimpleGraph.Walk.IsCycle.three_le_length {V : Type u} {G : } {v : V} {p : G.Walk v v} (hp : p.IsCycle) :
3 p.length
theorem SimpleGraph.Walk.cons_isCycle_iff {V : Type u} {G : } {u : V} {v : V} (p : G.Walk v u) (h : G.Adj u v) :
().IsCycle p.IsPath s(u, v)p.edges
theorem SimpleGraph.Walk.IsPath.tail {V : Type u} {G : } {u : V} {v : V} {p : G.Walk u v} (hp : p.IsPath) (hp' : ¬p.Nil) :
(p.tail hp').IsPath

### About paths #

instance SimpleGraph.Walk.instDecidableIsPathOfDecidableEq {V : Type u} {G : } [] {u : V} {v : V} (p : G.Walk u v) :
Decidable p.IsPath
Equations
• p.instDecidableIsPathOfDecidableEq = .mpr inferInstance
theorem SimpleGraph.Walk.IsPath.length_lt {V : Type u} {G : } [] {u : V} {v : V} {p : G.Walk u v} (hp : p.IsPath) :
p.length <

### Walk decompositions #

def SimpleGraph.Walk.takeUntil {V : Type u} {G : } [] {v : V} {w : V} (p : G.Walk v w) (u : V) :
u p.supportG.Walk v u

Given a vertex in the support of a path, give the path up until (and including) that vertex.

Equations
• One or more equations did not get rendered due to their size.
• SimpleGraph.Walk.nil.takeUntil x x_1 = .mpr SimpleGraph.Walk.nil
Instances For
def SimpleGraph.Walk.dropUntil {V : Type u} {G : } [] {v : V} {w : V} (p : G.Walk v w) (u : V) :
u p.supportG.Walk u w

Given a vertex in the support of a path, give the path from (and including) that vertex to the end. In other words, drop vertices from the front of a path until (and not including) that vertex.

Equations
• One or more equations did not get rendered due to their size.
• SimpleGraph.Walk.nil.dropUntil x x_1 = .mpr SimpleGraph.Walk.nil
Instances For
@[simp]
theorem SimpleGraph.Walk.take_spec {V : Type u} {G : } [] {u : V} {v : V} {w : V} (p : G.Walk v w) (h : u p.support) :
(p.takeUntil u h).append (p.dropUntil u h) = p

The takeUntil and dropUntil functions split a walk into two pieces. The lemma SimpleGraph.Walk.count_support_takeUntil_eq_one specifies where this split occurs.

theorem SimpleGraph.Walk.mem_support_iff_exists_append {V : Type u} {G : } {u : V} {v : V} {w : V} {p : G.Walk u v} :
w p.support ∃ (q : G.Walk u w) (r : G.Walk w v), p = q.append r
@[simp]
theorem SimpleGraph.Walk.count_support_takeUntil_eq_one {V : Type u} {G : } [] {u : V} {v : V} {w : V} (p : G.Walk v w) (h : u p.support) :
List.count u (p.takeUntil u h).support = 1
theorem SimpleGraph.Walk.count_edges_takeUntil_le_one {V : Type u} {G : } [] {u : V} {v : V} {w : V} (p : G.Walk v w) (h : u p.support) (x : V) :
List.count s(u, x) (p.takeUntil u h).edges 1
@[simp]
theorem SimpleGraph.Walk.takeUntil_copy {V : Type u} {G : } [] {u : V} {v : V} {w : V} {v' : V} {w' : V} (p : G.Walk v w) (hv : v = v') (hw : w = w') (h : u (p.copy hv hw).support) :
(p.copy hv hw).takeUntil u h = (p.takeUntil u ).copy hv
@[simp]
theorem SimpleGraph.Walk.dropUntil_copy {V : Type u} {G : } [] {u : V} {v : V} {w : V} {v' : V} {w' : V} (p : G.Walk v w) (hv : v = v') (hw : w = w') (h : u (p.copy hv hw).support) :
(p.copy hv hw).dropUntil u h = (p.dropUntil u ).copy hw
theorem SimpleGraph.Walk.support_takeUntil_subset {V : Type u} {G : } [] {u : V} {v : V} {w : V} (p : G.Walk v w) (h : u p.support) :
(p.takeUntil u h).support p.support
theorem SimpleGraph.Walk.support_dropUntil_subset {V : Type u} {G : } [] {u : V} {v : V} {w : V} (p : G.Walk v w) (h : u p.support) :
(p.dropUntil u h).support p.support
theorem SimpleGraph.Walk.darts_takeUntil_subset {V : Type u} {G : } [] {u : V} {v : V} {w : V} (p : G.Walk v w) (h : u p.support) :
(p.takeUntil u h).darts p.darts
theorem SimpleGraph.Walk.darts_dropUntil_subset {V : Type u} {G : } [] {u : V} {v : V} {w : V} (p : G.Walk v w) (h : u p.support) :
(p.dropUntil u h).darts p.darts
theorem SimpleGraph.Walk.edges_takeUntil_subset {V : Type u} {G : } [] {u : V} {v : V} {w : V} (p : G.Walk v w) (h : u p.support) :
(p.takeUntil u h).edges p.edges
theorem SimpleGraph.Walk.edges_dropUntil_subset {V : Type u} {G : } [] {u : V} {v : V} {w : V} (p : G.Walk v w) (h : u p.support) :
(p.dropUntil u h).edges p.edges
theorem SimpleGraph.Walk.length_takeUntil_le {V : Type u} {G : } [] {u : V} {v : V} {w : V} (p : G.Walk v w) (h : u p.support) :
(p.takeUntil u h).length p.length
theorem SimpleGraph.Walk.length_dropUntil_le {V : Type u} {G : } [] {u : V} {v : V} {w : V} (p : G.Walk v w) (h : u p.support) :
(p.dropUntil u h).length p.length
theorem SimpleGraph.Walk.IsTrail.takeUntil {V : Type u} {G : } [] {u : V} {v : V} {w : V} {p : G.Walk v w} (hc : p.IsTrail) (h : u p.support) :
(p.takeUntil u h).IsTrail
theorem SimpleGraph.Walk.IsTrail.dropUntil {V : Type u} {G : } [] {u : V} {v : V} {w : V} {p : G.Walk v w} (hc : p.IsTrail) (h : u p.support) :
(p.dropUntil u h).IsTrail
theorem SimpleGraph.Walk.IsPath.takeUntil {V : Type u} {G : } [] {u : V} {v : V} {w : V} {p : G.Walk v w} (hc : p.IsPath) (h : u p.support) :
(p.takeUntil u h).IsPath
theorem SimpleGraph.Walk.IsPath.dropUntil {V : Type u} {G : } [] {u : V} {v : V} {w : V} {p : G.Walk v w} (hc : p.IsPath) (h : u p.support) :
(p.dropUntil u h).IsPath
def SimpleGraph.Walk.rotate {V : Type u} {G : } [] {u : V} {v : V} (c : G.Walk v v) (h : u c.support) :
G.Walk u u

Rotate a loop walk such that it is centered at the given vertex.

Equations
• c.rotate h = (c.dropUntil u h).append (c.takeUntil u h)
Instances For
@[simp]
theorem SimpleGraph.Walk.support_rotate {V : Type u} {G : } [] {u : V} {v : V} (c : G.Walk v v) (h : u c.support) :
(c.rotate h).support.tail ~r c.support.tail
theorem SimpleGraph.Walk.rotate_darts {V : Type u} {G : } [] {u : V} {v : V} (c : G.Walk v v) (h : u c.support) :
(c.rotate h).darts ~r c.darts
theorem SimpleGraph.Walk.rotate_edges {V : Type u} {G : } [] {u : V} {v : V} (c : G.Walk v v) (h : u c.support) :
(c.rotate h).edges ~r c.edges
theorem SimpleGraph.Walk.IsTrail.rotate {V : Type u} {G : } [] {u : V} {v : V} {c : G.Walk v v} (hc : c.IsTrail) (h : u c.support) :
(c.rotate h).IsTrail
theorem SimpleGraph.Walk.IsCircuit.rotate {V : Type u} {G : } [] {u : V} {v : V} {c : G.Walk v v} (hc : c.IsCircuit) (h : u c.support) :
(c.rotate h).IsCircuit
theorem SimpleGraph.Walk.IsCycle.rotate {V : Type u} {G : } [] {u : V} {v : V} {c : G.Walk v v} (hc : c.IsCycle) (h : u c.support) :
(c.rotate h).IsCycle
theorem SimpleGraph.Walk.exists_boundary_dart {V : Type u} {G : } {u : V} {v : V} (p : G.Walk u v) (S : Set V) (uS : u S) (vS : vS) :
dp.darts, d.toProd.1 S d.toProd.2S

Given a set S and a walk w from u to v such that u ∈ S but v ∉ S, there exists a dart in the walk whose start is in S but whose end is not.

### Type of paths #

@[reducible, inline]
abbrev SimpleGraph.Path {V : Type u} (G : ) (u : V) (v : V) :

The type for paths between two vertices.

Equations
• G.Path u v = { p : G.Walk u v // p.IsPath }
Instances For
@[simp]
theorem SimpleGraph.Path.isPath {V : Type u} {G : } {u : V} {v : V} (p : G.Path u v) :
(p).IsPath
@[simp]
theorem SimpleGraph.Path.isTrail {V : Type u} {G : } {u : V} {v : V} (p : G.Path u v) :
(p).IsTrail
@[simp]
theorem SimpleGraph.Path.nil_coe {V : Type u} {G : } {u : V} :
SimpleGraph.Path.nil = SimpleGraph.Walk.nil
def SimpleGraph.Path.nil {V : Type u} {G : } {u : V} :
G.Path u u

The length-0 path at a vertex.

Equations
• SimpleGraph.Path.nil = SimpleGraph.Walk.nil,
Instances For
@[simp]
theorem SimpleGraph.Path.singleton_coe {V : Type u} {G : } {u : V} {v : V} (h : G.Adj u v) :
= SimpleGraph.Walk.cons h SimpleGraph.Walk.nil
def SimpleGraph.Path.singleton {V : Type u} {G : } {u : V} {v : V} (h : G.Adj u v) :
G.Path u v

The length-1 path between a pair of adjacent vertices.

Equations
Instances For
theorem SimpleGraph.Path.mk'_mem_edges_singleton {V : Type u} {G : } {u : V} {v : V} (h : G.Adj u v) :
s(u, v) ().edges
@[simp]
theorem SimpleGraph.Path.reverse_coe {V : Type u} {G : } {u : V} {v : V} (p : G.Path u v) :
p.reverse = (p).reverse
def SimpleGraph.Path.reverse {V : Type u} {G : } {u : V} {v : V} (p : G.Path u v) :
G.Path v u

The reverse of a path is another path. See also SimpleGraph.Walk.reverse.

Equations
• p.reverse = (p).reverse,
Instances For
theorem SimpleGraph.Path.count_support_eq_one {V : Type u} {G : } [] {u : V} {v : V} {w : V} {p : G.Path u v} (hw : w (p).support) :
List.count w (p).support = 1
theorem SimpleGraph.Path.count_edges_eq_one {V : Type u} {G : } [] {u : V} {v : V} {p : G.Path u v} (e : Sym2 V) (hw : e (p).edges) :
List.count e (p).edges = 1
@[simp]
theorem SimpleGraph.Path.nodup_support {V : Type u} {G : } {u : V} {v : V} (p : G.Path u v) :
(p).support.Nodup
theorem SimpleGraph.Path.loop_eq {V : Type u} {G : } {v : V} (p : G.Path v v) :
p = SimpleGraph.Path.nil
theorem SimpleGraph.Path.not_mem_edges_of_loop {V : Type u} {G : } {v : V} {e : Sym2 V} {p : G.Path v v} :
e(p).edges
theorem SimpleGraph.Path.cons_isCycle {V : Type u} {G : } {u : V} {v : V} (p : G.Path v u) (h : G.Adj u v) (he : s(u, v)(p).edges) :
().IsCycle

### Walks to paths #

def SimpleGraph.Walk.bypass {V : Type u} {G : } [] {u : V} {v : V} :
G.Walk u vG.Walk u v

Given a walk, produces a walk from it by bypassing subwalks between repeated vertices. The result is a path, as shown in SimpleGraph.Walk.bypass_isPath. This is packaged up in SimpleGraph.Walk.toPath.

Equations
• SimpleGraph.Walk.nil.bypass = SimpleGraph.Walk.nil
• ().bypass = let p' := q.bypass; if hs : u p'.support then p'.dropUntil u hs else
Instances For
@[simp]
theorem SimpleGraph.Walk.bypass_copy {V : Type u} {G : } [] {u : V} {v : V} {u' : V} {v' : V} (p : G.Walk u v) (hu : u = u') (hv : v = v') :
(p.copy hu hv).bypass = p.bypass.copy hu hv
theorem SimpleGraph.Walk.bypass_isPath {V : Type u} {G : } [] {u : V} {v : V} (p : G.Walk u v) :
p.bypass.IsPath
theorem SimpleGraph.Walk.length_bypass_le {V : Type u} {G : } [] {u : V} {v : V} (p : G.Walk u v) :
p.bypass.length p.length
theorem SimpleGraph.Walk.bypass_eq_self_of_length_le {V : Type u} {G : } [] {u : V} {v : V} (p : G.Walk u v) (h : p.length p.bypass.length) :
p.bypass = p
def SimpleGraph.Walk.toPath {V : Type u} {G : } [] {u : V} {v : V} (p : G.Walk u v) :
G.Path u v

Given a walk, produces a path with the same endpoints using SimpleGraph.Walk.bypass.

Equations
• p.toPath = p.bypass,
Instances For
theorem SimpleGraph.Walk.support_bypass_subset {V : Type u} {G : } [] {u : V} {v : V} (p : G.Walk u v) :
p.bypass.support p.support
theorem SimpleGraph.Walk.support_toPath_subset {V : Type u} {G : } [] {u : V} {v : V} (p : G.Walk u v) :
(p.toPath).support p.support
theorem SimpleGraph.Walk.darts_bypass_subset {V : Type u} {G : } [] {u : V} {v : V} (p : G.Walk u v) :
p.bypass.darts p.darts
theorem SimpleGraph.Walk.edges_bypass_subset {V : Type u} {G : } [] {u : V} {v : V} (p : G.Walk u v) :
p.bypass.edges p.edges
theorem SimpleGraph.Walk.darts_toPath_subset {V : Type u} {G : } [] {u : V} {v : V} (p : G.Walk u v) :
(p.toPath).darts p.darts
theorem SimpleGraph.Walk.edges_toPath_subset {V : Type u} {G : } [] {u : V} {v : V} (p : G.Walk u v) :
(p.toPath).edges p.edges

### Mapping paths #

def SimpleGraph.Walk.map {V : Type u} {V' : Type v} {G : } {G' : } (f : G →g G') {u : V} {v : V} :
G.Walk u vG'.Walk (f u) (f v)

Given a graph homomorphism, map walks to walks.

Equations
Instances For
@[simp]
theorem SimpleGraph.Walk.map_nil {V : Type u} {V' : Type v} {G : } {G' : } (f : G →g G') {u : V} :
SimpleGraph.Walk.map f SimpleGraph.Walk.nil = SimpleGraph.Walk.nil
@[simp]
theorem SimpleGraph.Walk.map_cons {V : Type u} {V' : Type v} {G : } {G' : } (f : G →g G') {u : V} {v : V} (p : G.Walk u v) {w : V} (h : G.Adj w u) :
@[simp]
theorem SimpleGraph.Walk.map_copy {V : Type u} {V' : Type v} {G : } {G' : } (f : G →g G') {u : V} {v : V} {u' : V} {v' : V} (p : G.Walk u v) (hu : u = u') (hv : v = v') :
SimpleGraph.Walk.map f (p.copy hu hv) = ().copy
@[simp]
theorem SimpleGraph.Walk.map_id {V : Type u} {G : } {u : V} {v : V} (p : G.Walk u v) (p : G.Walk u v) :
SimpleGraph.Walk.map SimpleGraph.Hom.id p = p
@[simp]
theorem SimpleGraph.Walk.map_map {V : Type u} {V' : Type v} {V'' : Type w} {G : } {G' : } {G'' : SimpleGraph V''} (f : G →g G') (f' : G' →g G'') {u : V} {v : V} (p : G.Walk u v) :
= SimpleGraph.Walk.map (f'.comp f) p
theorem SimpleGraph.Walk.map_eq_of_eq {V : Type u} {V' : Type v} {G : } {G' : } {u : V} {v : V} (p : G.Walk u v) {f : G →g G'} (f' : G →g G') (h : f = f') :
= ().copy

Unlike categories, for graphs vertex equality is an important notion, so needing to be able to work with equality of graph homomorphisms is a necessary evil.

@[simp]
theorem SimpleGraph.Walk.map_eq_nil_iff {V : Type u} {V' : Type v} {G : } {G' : } (f : G →g G') {u : V} {p : G.Walk u u} :
= SimpleGraph.Walk.nil p = SimpleGraph.Walk.nil
@[simp]
theorem SimpleGraph.Walk.length_map {V : Type u} {V' : Type v} {G : } {G' : } (f : G →g G') {u : V} {v : V} (p : G.Walk u v) :
().length = p.length
theorem SimpleGraph.Walk.map_append {V : Type u} {V' : Type v} {G : } {G' : } (f : G →g G') {u : V} {v : V} {w : V} (p : G.Walk u v) (q : G.Walk v w) :
SimpleGraph.Walk.map f (p.append q) = ().append ()
@[simp]
theorem SimpleGraph.Walk.reverse_map {V : Type u} {V' : Type v} {G : } {G' : } (f : G →g G') {u : V} {v : V} (p : G.Walk u v) :
().reverse = SimpleGraph.Walk.map f p.reverse
@[simp]
theorem SimpleGraph.Walk.support_map {V : Type u} {V' : Type v} {G : } {G' : } (f : G →g G') {u : V} {v : V} (p : G.Walk u v) :
().support = List.map (f) p.support
@[simp]
theorem SimpleGraph.Walk.darts_map {V : Type u} {V' : Type v} {G : } {G' : } (f : G →g G') {u : V} {v : V} (p : G.Walk u v) :
().darts = List.map f.mapDart p.darts
@[simp]
theorem SimpleGraph.Walk.edges_map {V : Type u} {V' : Type v} {G : } {G' : } (f : G →g G') {u : V} {v : V} (p : G.Walk u v) :
().edges = List.map (Sym2.map f) p.edges
theorem SimpleGraph.Walk.map_isPath_of_injective {V : Type u} {V' : Type v} {G : } {G' : } {f : G →g G'} {u : V} {v : V} {p : G.Walk u v} (hinj : ) (hp : p.IsPath) :
().IsPath
theorem SimpleGraph.Walk.IsPath.of_map {V : Type u} {V' : Type v} {G : } {G' : } {u : V} {v : V} {p : G.Walk u v} {f : G →g G'} (hp : ().IsPath) :
p.IsPath
theorem SimpleGraph.Walk.map_isPath_iff_of_injective {V : Type u} {V' : Type v} {G : } {G' : } {f : G →g G'} {u : V} {v : V} {p : G.Walk u v} (hinj : ) :
().IsPath p.IsPath
theorem SimpleGraph.Walk.map_isTrail_iff_of_injective {V : Type u} {V' : Type v} {G : } {G' : } {f : G →g G'} {u : V} {v : V} {p : G.Walk u v} (hinj : ) :
().IsTrail p.IsTrail
theorem SimpleGraph.Walk.map_isTrail_of_injective {V : Type u} {V' : Type v} {G : } {G' : } {f : G →g G'} {u : V} {v : V} {p : G.Walk u v} (hinj : ) :
p.IsTrail().IsTrail

Alias of the reverse direction of SimpleGraph.Walk.map_isTrail_iff_of_injective.

theorem SimpleGraph.Walk.map_isCycle_iff_of_injective {V : Type u} {V' : Type v} {G : } {G' : } {f : G →g G'} {u : V} {p : G.Walk u u} (hinj : ) :
().IsCycle p.IsCycle
theorem SimpleGraph.Walk.IsCycle.map {V : Type u} {V' : Type v} {G : } {G' : } {f : G →g G'} {u : V} {p : G.Walk u u} (hinj : ) :
p.IsCycle().IsCycle

Alias of the reverse direction of SimpleGraph.Walk.map_isCycle_iff_of_injective.

theorem SimpleGraph.Walk.map_injective_of_injective {V : Type u} {V' : Type v} {G : } {G' : } {f : G →g G'} (hinj : ) (u : V) (v : V) :
@[reducible, inline]
abbrev SimpleGraph.Walk.mapLe {V : Type u} {G : } {G' : } (h : G G') {u : V} {v : V} (p : G.Walk u v) :
G'.Walk u v

The specialization of SimpleGraph.Walk.map for mapping walks to supergraphs.

Equations
Instances For
@[simp]
theorem SimpleGraph.Walk.mapLe_isTrail {V : Type u} {G : } {G' : } (h : G G') {u : V} {v : V} {p : G.Walk u v} :
().IsTrail p.IsTrail
theorem SimpleGraph.Walk.IsTrail.mapLe {V : Type u} {G : } {G' : } (h : G G') {u : V} {v : V} {p : G.Walk u v} :
p.IsTrail().IsTrail

Alias of the reverse direction of SimpleGraph.Walk.mapLe_isTrail.

theorem SimpleGraph.Walk.IsTrail.of_mapLe {V : Type u} {G : } {G' : } (h : G G') {u : V} {v : V} {p : G.Walk u v} :
().IsTrailp.IsTrail

Alias of the forward direction of SimpleGraph.Walk.mapLe_isTrail.

@[simp]
theorem SimpleGraph.Walk.mapLe_isPath {V : Type u} {G : } {G' : } (h : G G') {u : V} {v : V} {p : G.Walk u v} :
().IsPath p.IsPath
theorem SimpleGraph.Walk.IsPath.of_mapLe {V : Type u} {G : } {G' : } (h : G G') {u : V} {v : V} {p : G.Walk u v} :
().IsPathp.IsPath

Alias of the forward direction of SimpleGraph.Walk.mapLe_isPath.

theorem SimpleGraph.Walk.IsPath.mapLe {V : Type u} {G : } {G' : } (h : G G') {u : V} {v : V} {p : G.Walk u v} :
p.IsPath().IsPath

Alias of the reverse direction of SimpleGraph.Walk.mapLe_isPath.

@[simp]
theorem SimpleGraph.Walk.mapLe_isCycle {V : Type u} {G : } {G' : } (h : G G') {u : V} {p : G.Walk u u} :
().IsCycle p.IsCycle
theorem SimpleGraph.Walk.IsCycle.mapLe {V : Type u} {G : } {G' : } (h : G G') {u : V} {p : G.Walk u u} :
p.IsCycle().IsCycle

Alias of the reverse direction of SimpleGraph.Walk.mapLe_isCycle.

theorem SimpleGraph.Walk.IsCycle.of_mapLe {V : Type u} {G : } {G' : } (h : G G') {u : V} {p : G.Walk u u} :
().IsCyclep.IsCycle

Alias of the forward direction of SimpleGraph.Walk.mapLe_isCycle.

@[simp]
theorem SimpleGraph.Path.map_coe {V : Type u} {V' : Type v} {G : } {G' : } (f : G →g G') (hinj : ) {u : V} {v : V} (p : G.Path u v) :
(SimpleGraph.Path.map f hinj p) =
def SimpleGraph.Path.map {V : Type u} {V' : Type v} {G : } {G' : } (f : G →g G') (hinj : ) {u : V} {v : V} (p : G.Path u v) :
G'.Path (f u) (f v)

Given an injective graph homomorphism, map paths to paths.

Equations
Instances For
theorem SimpleGraph.Path.map_injective {V : Type u} {V' : Type v} {G : } {G' : } {f : G →g G'} (hinj : ) (u : V) (v : V) :
@[simp]
theorem SimpleGraph.Path.mapEmbedding_coe {V : Type u} {V' : Type v} {G : } {G' : } (f : G ↪g G') {u : V} {v : V} (p : G.Path u v) :
= SimpleGraph.Walk.map f.toHom p
def SimpleGraph.Path.mapEmbedding {V : Type u} {V' : Type v} {G : } {G' : } (f : G ↪g G') {u : V} {v : V} (p : G.Path u v) :
G'.Path (f u) (f v)

Given a graph embedding, map paths to paths.

Equations
Instances For
theorem SimpleGraph.Path.mapEmbedding_injective {V : Type u} {V' : Type v} {G : } {G' : } (f : G ↪g G') (u : V) (v : V) :

### Transferring between graphs

def SimpleGraph.Walk.transfer {V : Type u} {G : } {u : V} {v : V} (p : G.Walk u v) (H : ) (h : ep.edges, e H.edgeSet) :
H.Walk u v

The walk p transferred to lie in H, given that H contains its edges.

Equations
Instances For
theorem SimpleGraph.Walk.transfer_self {V : Type u} {G : } {u : V} {v : V} (p : G.Walk u v) :
p.transfer G = p
theorem SimpleGraph.Walk.transfer_eq_map_of_le {V : Type u} {G : } {u : V} {v : V} (p : G.Walk u v) {H : } (hp : ep.edges, e H.edgeSet) (GH : G H) :
p.transfer H hp =
@[simp]
theorem SimpleGraph.Walk.edges_transfer {V : Type u} {G : } {u : V} {v : V} (p : G.Walk u v) {H : } (hp : ep.edges, e H.edgeSet) :
(p.transfer H hp).edges = p.edges
@[simp]
theorem SimpleGraph.Walk.support_transfer {V : Type u} {G : } {u : V} {v : V} (p : G.Walk u v) {H : } (hp : ep.edges, e H.edgeSet) :
(p.transfer H hp).support = p.support
@[simp]
theorem SimpleGraph.Walk.length_transfer {V : Type u} {G : } {u : V} {v : V} (p : G.Walk u v) {H : } (hp : ep.edges, e H.edgeSet) :
(p.transfer H hp).length = p.length
theorem SimpleGraph.Walk.IsPath.transfer {V : Type u} {G : } {u : V} {v : V} {p : G.Walk u v} {H : } (hp : ep.edges, e H.edgeSet) (pp : p.IsPath) :
(p.transfer H hp).IsPath
theorem SimpleGraph.Walk.IsCycle.transfer {V : Type u} {G : } {u : V} {H : } {q : G.Walk u u} (qc : q.IsCycle) (hq : eq.edges, e H.edgeSet) :
(q.transfer H hq).IsCycle
@[simp]
theorem SimpleGraph.Walk.transfer_transfer {V : Type u} {G : } {u : V} {v : V} (p : G.Walk u v) {H : } (hp : ep.edges, e H.edgeSet) {K : } (hp' : e(p.transfer H hp).edges, e K.edgeSet) :
(p.transfer H hp).transfer K hp' = p.transfer K
@[simp]
theorem SimpleGraph.Walk.transfer_append {V : Type u} {G : } {u : V} {v : V} (p : G.Walk u v) {H : } {w : V} (q : G.Walk v w) (hpq : e(p.append q).edges, e H.edgeSet) :
(p.append q).transfer H hpq = (p.transfer H ).append (q.transfer H )
@[simp]
theorem SimpleGraph.Walk.reverse_transfer {V : Type u} {G : } {u : V} {v : V} (p : G.Walk u v) {H : } (hp : ep.edges, e H.edgeSet) :
(p.transfer H hp).reverse = p.reverse.transfer H

## Deleting edges #

@[reducible, inline]
abbrev SimpleGraph.Walk.toDeleteEdges {V : Type u} {G : } (s : Set (Sym2 V)) {v : V} {w : V} (p : G.Walk v w) (hp : ep.edges, es) :
(G.deleteEdges s).Walk v w

Given a walk that avoids a set of edges, produce a walk in the graph with those edges deleted.

Equations
• = p.transfer (G.deleteEdges s)
Instances For
@[simp]
theorem SimpleGraph.Walk.toDeleteEdges_nil {V : Type u} {G : } (s : Set (Sym2 V)) {v : V} (hp : eSimpleGraph.Walk.nil.edges, es) :
SimpleGraph.Walk.toDeleteEdges s SimpleGraph.Walk.nil hp = SimpleGraph.Walk.nil
@[simp]
theorem SimpleGraph.Walk.toDeleteEdges_cons {V : Type u} {G : } (s : Set (Sym2 V)) {u : V} {v : V} {w : V} (h : G.Adj u v) (p : G.Walk v w) (hp : e().edges, es) :
@[reducible, inline]
abbrev SimpleGraph.Walk.toDeleteEdge {V : Type u} {G : } {v : V} {w : V} (e : Sym2 V) (p : G.Walk v w) (hp : ep.edges) :
(G.deleteEdges {e}).Walk v w

Given a walk that avoids an edge, create a walk in the subgraph with that edge deleted. This is an abbreviation for SimpleGraph.Walk.toDeleteEdges.

Equations
Instances For
@[simp]
theorem SimpleGraph.Walk.map_toDeleteEdges_eq {V : Type u} {G : } {v : V} {w : V} (s : Set (Sym2 V)) {p : G.Walk v w} (hp : ep.edges, es) :
theorem SimpleGraph.Walk.IsPath.toDeleteEdges {V : Type u} {G : } {v : V} {w : V} (s : Set (Sym2 V)) {p : G.Walk v w} (h : p.IsPath) (hp : ep.edges, es) :
().IsPath
theorem SimpleGraph.Walk.IsCycle.toDeleteEdges {V : Type u} {G : } {v : V} (s : Set (Sym2 V)) {p : G.Walk v v} (h : p.IsCycle) (hp : ep.edges, es) :
().IsCycle
@[simp]
theorem SimpleGraph.Walk.toDeleteEdges_copy {V : Type u} {G : } {v : V} {u : V} {u' : V} {v' : V} (s : Set (Sym2 V)) (p : G.Walk u v) (hu : u = u') (hv : v = v') (h : e(p.copy hu hv).edges, es) :
SimpleGraph.Walk.toDeleteEdges s (p.copy hu hv) h = ().copy hu hv

## Reachable and Connected#

def SimpleGraph.Reachable {V : Type u} (G : ) (u : V) (v : V) :

Two vertices are reachable if there is a walk between them. This is equivalent to Relation.ReflTransGen of G.Adj. See SimpleGraph.reachable_iff_reflTransGen.

Equations
Instances For
theorem SimpleGraph.reachable_iff_nonempty_univ {V : Type u} {G : } {u : V} {v : V} :
G.Reachable u v Set.univ.Nonempty
theorem SimpleGraph.Reachable.elim {V : Type u} {G : } {p : Prop} {u : V} {v : V} (h : G.Reachable u v) (hp : G.Walk u vp) :
p
theorem SimpleGraph.Reachable.elim_path {V : Type u} {G : } {p : Prop} {u : V} {v : V} (h : G.Reachable u v) (hp : G.Path u vp) :
p
theorem SimpleGraph.Walk.reachable {V : Type u} {G : } {u : V} {v : V} (p : G.Walk u v) :
G.Reachable u v
theorem SimpleGraph.Adj.reachable {V : Type u} {G : } {u : V} {v : V} (h : G.Adj u v) :
G.Reachable u v
theorem SimpleGraph.Reachable.refl {V : Type u} {G : } (u : V) :
G.Reachable u u
theorem SimpleGraph.Reachable.rfl {V : Type u} {G : } {u : V} :
G.Reachable u u
theorem SimpleGraph.Reachable.symm {V : Type u} {G : } {u : V} {v : V} (huv : G.Reachable u v) :
G.Reachable v u
theorem SimpleGraph.reachable_comm {V : Type u} {G : } {u : V} {v : V} :
G.Reachable u v G.Reachable v u
theorem SimpleGraph.Reachable.trans {V : Type u} {G : } {u : V} {v : V} {w : V} (huv : G.Reachable u v) (hvw : G.Reachable v w) :
G.Reachable u w
theorem SimpleGraph.reachable_iff_reflTransGen {V : Type u} {G : } (u : V) (v : V) :
G.Reachable u v Relation.ReflTransGen G.Adj u v
theorem SimpleGraph.Reachable.map {V : Type u} {V' : Type v} {u : V} {v : V} {G : } {G' : } (f : G →g G') (h : G.Reachable u v) :
G'.Reachable (f u) (f v)
theorem SimpleGraph.Reachable.mono {V : Type u} {u : V} {v : V} {G : } {G' : } (h : G G') (Guv : G.Reachable u v) :
G'.Reachable u v
theorem SimpleGraph.Iso.reachable_iff {V : Type u} {V' : Type v} {G : } {G' : } {φ : G ≃g G'} {u : V} {v : V} :
G'.Reachable (φ u) (φ v) G.Reachable u v
theorem SimpleGraph.Iso.symm_apply_reachable {V : Type u} {V' : Type v} {G : } {G' : } {φ : G ≃g G'} {u : V} {v : V'} :
G.Reachable (φ.symm v) u G'.Reachable v (φ u)
theorem SimpleGraph.reachable_is_equivalence {V : Type u} (G : ) :
Equivalence G.Reachable
def SimpleGraph.reachableSetoid {V : Type u} (G : ) :

The equivalence relation on vertices given by SimpleGraph.Reachable.

Equations
• G.reachableSetoid = { r := G.Reachable, iseqv := }
Instances For
def SimpleGraph.Preconnected {V : Type u} (G : ) :

A graph is preconnected if every pair of vertices is reachable from one another.

Equations
• G.Preconnected = ∀ (u v : V), G.Reachable u v
Instances For
theorem SimpleGraph.Preconnected.map {V : Type u} {V' : Type v} {G : } {H : } (f : G →g H) (hf : ) (hG : G.Preconnected) :
H.Preconnected
theorem SimpleGraph.Preconnected.mono {V : Type u} {G : } {G' : } (h : G G') (hG : G.Preconnected) :
G'.Preconnected
theorem SimpleGraph.top_preconnected {V : Type u} :
.Preconnected
theorem SimpleGraph.Iso.preconnected_iff {V : Type u} {V' : Type v} {G : } {H : } (e : G ≃g H) :
G.Preconnected H.Preconnected
theorem SimpleGraph.connected_iff {V : Type u} (G : ) :
G.Connected G.Preconnected
structure SimpleGraph.Connected {V : Type u} (G : ) :

A graph is connected if it's preconnected and contains at least one vertex. This follows the convention observed by mathlib that something is connected iff it has exactly one connected component.

There is a CoeFun instance so that h u v can be used instead of h.Preconnected u v.

• preconnected : G.Preconnected
• nonempty :
Instances For
theorem SimpleGraph.Connected.preconnected {V : Type u} {G : } (self : G.Connected) :
G.Preconnected
theorem SimpleGraph.Connected.nonempty {V : Type u} {G : } (self : G.Connected) :
theorem SimpleGraph.connected_iff_exists_forall_reachable {V : Type u} (G : ) :
G.Connected ∃ (v : V), ∀ (w : V), G.Reachable v w
instance SimpleGraph.instCoeFunConnectedForallForallReachable {V : Type u} (G : ) :
CoeFun G.Connected fun (x : G.Connected) => ∀ (u v : V), G.Reachable u v
Equations
• G.instCoeFunConnectedForallForallReachable = { coe := }
theorem SimpleGraph.Connected.map {V : Type u} {V' : Type v} {G : } {H : } (f : G →g H) (hf : ) (hG : G.Connected) :
H.Connected
theorem SimpleGraph.Connected.mono {V : Type u} {G : } {G' : } (h : G G') (hG : G.Connected) :
G'.Connected
theorem SimpleGraph.top_connected {V : Type u} [] :
.Connected
theorem SimpleGraph.Iso.connected_iff {V : Type u} {V' : Type v} {G : } {H : } (e : G ≃g H) :
G.Connected H.Connected

The quotient of V by the SimpleGraph.Reachable relation gives the connected components of a graph.

Equations
• G.ConnectedComponent = Quot G.Reachable
Instances For
def SimpleGraph.connectedComponentMk {V : Type u} (G : ) (v : V) :
G.ConnectedComponent

Gives the connected component containing a particular vertex.

Equations
• G.connectedComponentMk v = Quot.mk G.Reachable v
Instances For
@[simp]
theorem SimpleGraph.ConnectedComponent.inhabited_default {V : Type u} {G : } [] :
default = G.connectedComponentMk default
instance SimpleGraph.ConnectedComponent.inhabited {V : Type u} {G : } [] :
Inhabited G.ConnectedComponent
Equations
• SimpleGraph.ConnectedComponent.inhabited = { default := G.connectedComponentMk default }
theorem SimpleGraph.ConnectedComponent.ind {V : Type u} {G : } {β : G.ConnectedComponentProp} (h : ∀ (v : V), β (G.connectedComponentMk v)) (c : G.ConnectedComponent) :
β c
theorem SimpleGraph.ConnectedComponent.ind₂ {V : Type u} {G : } {β : G.ConnectedComponentG.ConnectedComponentProp} (h : ∀ (v w : V), β (G.connectedComponentMk v) (G.connectedComponentMk w)) (c : G.ConnectedComponent) (d : G.ConnectedComponent) :
β c d
theorem SimpleGraph.ConnectedComponent.sound {V : Type u} {G : } {v : V} {w : V} :
G.Reachable v wG.connectedComponentMk v = G.connectedComponentMk w
theorem SimpleGraph.ConnectedComponent.exact {V : Type u} {G : } {v : V} {w : V} :
G.connectedComponentMk v = G.connectedComponentMk wG.Reachable v w
@[simp]
theorem SimpleGraph.ConnectedComponent.eq {V : Type u} {G : } {v : V} {w : V} :
G.connectedComponentMk v = G.connectedComponentMk w G.Reachable v w
theorem SimpleGraph.ConnectedComponent.connectedComponentMk_eq_of_adj {V : Type u} {G : } {v : V} {w : V} (a : G.Adj v w) :
G.connectedComponentMk v = G.connectedComponentMk w
def SimpleGraph.ConnectedComponent.lift {V : Type u} {G : } {β : Sort u_1} (f : Vβ) (h : ∀ (v w : V) (p : G.Walk v w), p.IsPathf v = f w) :
G.ConnectedComponentβ

The ConnectedComponent specialization of Quot.lift. Provides the stronger assumption that the vertices are connected by a path.

Equations
Instances For
@[simp]
theorem SimpleGraph.ConnectedComponent.lift_mk {V : Type u} {G : } {β : Sort u_1} {f : Vβ} {h : ∀ (v w : V) (p : G.Walk v w), p.IsPathf v = f w} {v : V} :
SimpleGraph.ConnectedComponent.lift f h (G.connectedComponentMk v) = f v
theorem SimpleGraph.ConnectedComponent.exists {V : Type u} {G : } {p : G.ConnectedComponentProp} :
(∃ (c : G.ConnectedComponent), p c) ∃ (v : V), p (G.connectedComponentMk v)
theorem SimpleGraph.ConnectedComponent.forall {V : Type u} {G : } {p : G.ConnectedComponentProp} :
(∀ (c : G.ConnectedComponent), p c) ∀ (v : V), p (G.connectedComponentMk v)
theorem SimpleGraph.Preconnected.subsingleton_connectedComponent {V : Type u} {G : } (h : G.Preconnected) :
Subsingleton G.ConnectedComponent
def SimpleGraph.ConnectedComponent.map {V : Type u} {V' : Type v} {G : } {G' : } (φ : G →g G') (C : G.ConnectedComponent) :
G'.ConnectedComponent

The map on connected components induced by a graph homomorphism.

Equations
Instances For
@[simp]
theorem SimpleGraph.ConnectedComponent.map_mk {V : Type u} {V' : Type v} {G : } {G' : } (φ : G →g G') (v : V) :
SimpleGraph.ConnectedComponent.map φ (G.connectedComponentMk v) = G'.connectedComponentMk (φ v)
@[simp]
theorem SimpleGraph.ConnectedComponent.map_id {V : Type u} {G : } (C : G.ConnectedComponent) :
SimpleGraph.ConnectedComponent.map SimpleGraph.Hom.id C = C
@[simp]
theorem SimpleGraph.ConnectedComponent.map_comp {V : Type u} {V' : Type v} {V'' : Type w} {G : } {G' : } {G'' : SimpleGraph V''} (C : G.ConnectedComponent) (φ : G →g G') (ψ : G' →g G'') :
@[simp]
theorem SimpleGraph.ConnectedComponent.iso_image_comp_eq_map_iff_eq_comp {V : Type u} {V' : Type v} {G : } {G' : } {φ : G ≃g G'} {v : V} {C : G.ConnectedComponent} :
G'.connectedComponentMk (φ v) = SimpleGraph.ConnectedComponent.map .toRelHom C G.connectedComponentMk v = C
@[simp]
theorem SimpleGraph.ConnectedComponent.iso_inv_image_comp_eq_iff_eq_map {V : Type u} {V' : Type v} {G : } {G' : } {φ : G ≃g G'} {v' : V'} {C : G.ConnectedComponent} :
G.connectedComponentMk (φ.symm v') = C G'.connectedComponentMk v' = SimpleGraph.ConnectedComponent.map .toRelHom C
@[simp]
theorem SimpleGraph.Iso.connectedComponentEquiv_symm_apply {V : Type u} {V' : Type v} {G : } {G' : } (φ : G ≃g G') (C : G'.ConnectedComponent) :
φ.connectedComponentEquiv.symm C = SimpleGraph.ConnectedComponent.map (RelIso.toRelEmbedding φ.symm).toRelHom C
@[simp]
theorem SimpleGraph.Iso.connectedComponentEquiv_apply {V : Type u} {V' : Type v} {G : } {G' : } (φ : G ≃g G') (C : G.ConnectedComponent) :
φ.connectedComponentEquiv C = SimpleGraph.ConnectedComponent.map .toRelHom C
def SimpleGraph.Iso.connectedComponentEquiv {V : Type u} {V' : Type v} {G : } {G' : } (φ : G ≃g G') :
G.ConnectedComponent G'.ConnectedComponent

An isomorphism of graphs induces a bijection of connected components.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem SimpleGraph.Iso.connectedComponentEquiv_refl {V : Type u} {G : } :
SimpleGraph.Iso.refl.connectedComponentEquiv = Equiv.refl G.ConnectedComponent
@[simp]
theorem SimpleGraph.Iso.connectedComponentEquiv_symm {V : Type u} {V' : Type v} {G : } {G' : } (φ : G ≃g G') :
φ.symm.connectedComponentEquiv = φ.connectedComponentEquiv.symm
@[simp]
theorem SimpleGraph.Iso.connectedComponentEquiv_trans {V : Type u} {V' : Type v} {V'' : Type w} {G : } {G' : } {G'' : SimpleGraph V''} (φ : G ≃g G') (φ' : G' ≃g G'') :
= φ.connectedComponentEquiv.trans φ'.connectedComponentEquiv
def SimpleGraph.ConnectedComponent.supp {V : Type u} {G : } (C : G.ConnectedComponent) :
Set V

The set of vertices in a connected component of a graph.

Equations
• C.supp = {v : V | G.connectedComponentMk v = C}
Instances For
theorem SimpleGraph.ConnectedComponent.supp_injective {V : Type u} {G : } :
Function.Injective SimpleGraph.ConnectedComponent.supp
@[simp]
theorem SimpleGraph.ConnectedComponent.supp_inj {V : Type u} {G : } {C : G.ConnectedComponent} {D : G.ConnectedComponent} :
C.supp = D.supp C = D
instance SimpleGraph.ConnectedComponent.instSetLike {V : Type u} {G : } :
SetLike G.ConnectedComponent V
Equations
• SimpleGraph.ConnectedComponent.instSetLike = { coe := SimpleGraph.ConnectedComponent.supp, coe_injective' := }
@[simp]
theorem SimpleGraph.ConnectedComponent.mem_supp_iff {V : Type u} {G : } (C : G.ConnectedComponent) (v : V) :
v C.supp G.connectedComponentMk v = C
theorem SimpleGraph.ConnectedComponent.connectedComponentMk_mem {V : Type u} {G : } {v : V} :
v G.connectedComponentMk v
def SimpleGraph.ConnectedComponent.isoEquivSupp {V : Type u} {V' : Type v} {G : } {G' : } (φ : G ≃g G') (C : G.ConnectedComponent) :
C.supp (φ.connectedComponentEquiv C).supp

The equivalence between connected components, induced by an isomorphism of graphs, itself defines an equivalence on the supports of each connected component.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem SimpleGraph.Preconnected.set_univ_walk_nonempty {V : Type u} {G : } (hconn : G.Preconnected) (u : V) (v : V) :
Set.univ.Nonempty
theorem SimpleGraph.Connected.set_univ_walk_nonempty {V : Type u} {G : } (hconn : G.Connected) (u : V) (v : V) :
Set.univ.Nonempty

### Walks as subgraphs #

def SimpleGraph.Walk.toSubgraph {V : Type u} {G : } {u : V} {v : V} :
G.Walk u vG.Subgraph

The subgraph consisting of the vertices and edges of the walk.

Equations
• SimpleGraph.Walk.nil.toSubgraph = G.singletonSubgraph u
• ().toSubgraph = G.subgraphOfAdj h q.toSubgraph
Instances For
theorem SimpleGraph.Walk.toSubgraph_cons_nil_eq_subgraphOfAdj {V : Type u} {G : } {u : V} {v : V} (h : G.Adj u v) :
(SimpleGraph.Walk.cons h SimpleGraph.Walk.nil).toSubgraph = G.subgraphOfAdj h
theorem SimpleGraph.Walk.mem_verts_toSubgraph {V : Type u} {G : } {u : V} {v : V} {w : V} (p : G.Walk u v) :
w p.toSubgraph.verts w p.support
theorem SimpleGraph.Walk.start_mem_verts_toSubgraph {V : Type u} {G : } {u : V} {v : V} (p : G.Walk u v) :
u p.toSubgraph.verts
theorem SimpleGraph.Walk.end_mem_verts_toSubgraph {V : Type u} {G : } {u : V} {v : V} (p : G.Walk u v) :
v p.toSubgraph.verts
@[simp]
theorem SimpleGraph.Walk.verts_toSubgraph {V : Type u} {G : } {u : V} {v : V} (p : G.Walk u v) :
p.toSubgraph.verts = {w : V | w p.support}
theorem SimpleGraph.Walk.mem_edges_toSubgraph {V : Type u} {G : } {u : V} {v : V} (p : G.Walk u v) {e : Sym2 V} :
e p.toSubgraph.edgeSet e p.edges
@[simp]
theorem SimpleGraph.Walk.edgeSet_toSubgraph {V : Type u} {G : } {u : V} {v : V} (p : G.Walk u v) :
p.toSubgraph.edgeSet = {e : Sym2 V | e p.edges}
@[simp]
theorem SimpleGraph.Walk.toSubgraph_append {V : Type u} {G : } {u : V} {v : V} {w : V} (p : G.Walk u v) (q : G.Walk v w) :
(p.append q).toSubgraph = p.toSubgraph q.toSubgraph
@[simp]
theorem SimpleGraph.Walk.toSubgraph_reverse {V : Type u} {G : } {u : V} {v : V} (p : G.Walk u v) :
p.reverse.toSubgraph = p.toSubgraph
@[simp]
theorem SimpleGraph.Walk.toSubgraph_rotate {V : Type u} {G : } {u : V} {v : V} [] (c : G.Walk v v) (h : u c.support) :
(c.rotate h).toSubgraph = c.toSubgraph
@[simp]
theorem SimpleGraph.Walk.toSubgraph_map {V : Type u} {V' : Type v} {G : } {G' : } {u : V} {v : V} (f : G →g G') (p : G.Walk u v) :
().toSubgraph = SimpleGraph.Subgraph.map f p.toSubgraph
@[simp]
theorem SimpleGraph.Walk.finite_neighborSet_toSubgraph {V : Type u} {G : } {u : V} {v : V} {w : V} (p : G.Walk u v) :
(p.toSubgraph.neighborSet w).Finite
theorem SimpleGraph.Walk.toSubgraph_le_induce_support {V : Type u} {G : } {u : V} {v : V} (p : G.Walk u v) :
p.toSubgraph .induce {v_1 : V | v_1 p.support}

### Walks of a given length #

theorem SimpleGraph.set_walk_self_length_zero_eq {V : Type u} {G : } (u : V) :
{p : G.Walk u u | p.length = 0} = {SimpleGraph.Walk.nil}
theorem SimpleGraph.set_walk_length_zero_eq_of_ne {V : Type u} {G : } {u : V} {v : V} (h : u v) :
{p : G.Walk u v | p.length = 0} =
theorem SimpleGraph.set_walk_length_succ_eq {V : Type u} {G : } (u : V) (v : V) (n : ) :
{p : G.Walk u v | p.length = n.succ} = ⋃ (w : V), ⋃ (h : G.Adj u w), '' {p' : G.Walk w v | p'.length = n}
@[simp]
theorem SimpleGraph.walkLengthTwoEquivCommonNeighbors_symm_apply_coe {V : Type u} (G : ) (u : V) (v : V) (w : (G.commonNeighbors u v)) :
((G.walkLengthTwoEquivCommonNeighbors u v).symm w) = .concat
@[simp]
theorem SimpleGraph.walkLengthTwoEquivCommonNeighbors_apply_coe {V : Type u} (G : ) (u : V) (v : V) (p : { p : G.Walk u v // p.length = 2 }) :
((G.walkLengthTwoEquivCommonNeighbors u v) p) = (p).getVert 1
def SimpleGraph.walkLengthTwoEquivCommonNeighbors {V : Type u} (G : ) (u : V) (v : V) :
{ p : G.Walk u v // p.length = 2 } (G.commonNeighbors u v)

Walks of length two from u to v correspond bijectively to common neighbours of u and v. Note that u and v may be the same.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def SimpleGraph.finsetWalkLength {V : Type u} (G : ) [] [G.LocallyFinite] (n : ) (u : V) (v : V) :
Finset (G.Walk u v)

The Finset of length-n walks from u to v. This is used to give {p : G.walk u v | p.length = n} a Fintype instance, and it can also be useful as a recursive description of this set when V is finite.

See SimpleGraph.coe_finsetWalkLength_eq for the relationship between this Finset and the set of length-n walks.

Equations
• One or more equations did not get rendered due to their size.
• G.finsetWalkLength 0 u v = if h : u = v then {SimpleGraph.Walk.nil} else
Instances For
theorem SimpleGraph.coe_finsetWalkLength_eq {V : Type u} (G : ) [] [G.LocallyFinite] (n : ) (u : V) (v : V) :
(G.finsetWalkLength n u v) = {p : G.Walk u v | p.length = n}
theorem SimpleGraph.Walk.mem_finsetWalkLength_iff_length_eq {V : Type u} {G : } [] [G.LocallyFinite] {n : } {u : V} {v : V} (p : G.Walk u v) :
p G.finsetWalkLength n u v p.length = n
instance SimpleGraph.fintypeSetWalkLength {V : Type u} (G : ) [] [G.LocallyFinite] (u : V) (v : V) (n : ) :
Fintype {p : G.Walk u v | p.length = n}
Equations
instance SimpleGraph.fintypeSubtypeWalkLength {V : Type u} (G : ) [] [G.LocallyFinite] (u : V) (v : V) (n : ) :
Fintype { p : G.Walk u v // p.length = n }
Equations
• G.fintypeSubtypeWalkLength u v n = G.fintypeSetWalkLength u v n
theorem SimpleGraph.set_walk_length_toFinset_eq {V : Type u} (G : ) [] [G.LocallyFinite] (n : ) (u : V) (v : V) :
{p : G.Walk u v | p.length = n}.toFinset = G.finsetWalkLength n u v
theorem SimpleGraph.card_set_walk_length_eq {V : Type u} (G : ) [] [G.LocallyFinite] (u : V) (v : V) (n : ) :
Fintype.card {p : G.Walk u v | p.length = n} = (G.finsetWalkLength n u v).card
instance SimpleGraph.fintypeSetPathLength {V : Type u} (G : ) [] [G.LocallyFinite] (u : V) (v : V) (n : ) :
Fintype {p : G.Walk u v | p.IsPath p.length = n}
Equations
theorem SimpleGraph.reachable_iff_exists_finsetWalkLength_nonempty {V : Type u} (G : ) [] [] [DecidableRel G.Adj] (u : V) (v : V) :
G.Reachable u v ∃ (n : Fin ()), (G.finsetWalkLength (n) u v).Nonempty
instance SimpleGraph.instDecidableRelReachable {V : Type u} (G : ) [] [] [DecidableRel G.Adj] :
DecidableRel G.Reachable
Equations
• G.instDecidableRelReachable u v = decidable_of_iff' (∃ (n : Fin ()), (G.finsetWalkLength (n) u v).Nonempty)
instance SimpleGraph.instFintypeConnectedComponent {V : Type u} (G : ) [] [] [DecidableRel G.Adj] :
Fintype G.ConnectedComponent
Equations
instance SimpleGraph.instDecidablePreconnected {V : Type u} (G : ) [] [] [DecidableRel G.Adj] :
Decidable G.Preconnected
Equations
instance SimpleGraph.instDecidableConnected {V : Type u} (G : ) [] [] [DecidableRel G.Adj] :
Decidable G.Connected
Equations
• G.instDecidableConnected = .mpr (.mpr inferInstance)

### Bridge edges #

def SimpleGraph.IsBridge {V : Type u} (G : ) (e : Sym2 V) :

An edge of a graph is a bridge if, after removing it, its incident vertices are no longer reachable from one another.

Equations
• G.IsBridge e = (e G.edgeSet Sym2.lift fun (v w : V) => ¬().Reachable v w, e)
Instances For
theorem SimpleGraph.isBridge_iff {V : Type u} {G : } {u : V} {v : V} :
G.IsBridge s(u, v) G.Adj u v ¬(G \ SimpleGraph.fromEdgeSet {s(u, v)}).Reachable u v
theorem SimpleGraph.reachable_delete_edges_iff_exists_walk {V : Type u} {G : } {v : V} {w : V} :
(G \ SimpleGraph.fromEdgeSet {s(v, w)}).Reachable v w ∃ (p : G.Walk v w), s(v, w)p.edges
theorem SimpleGraph.isBridge_iff_adj_and_forall_walk_mem_edges {V : Type u} {G : } {v : V} {w : V} :
G.IsBridge s(v, w) G.Adj v w ∀ (p : G.Walk v w), s(v, w) p.edges
theorem SimpleGraph.reachable_deleteEdges_iff_exists_cycle.aux {V : Type u} {G : } [] {u : V} {v : V} {w : V} (hb : ∀ (p : G.Walk v w), s(v, w) p.edges) (c : G.Walk u u) (hc : c.IsTrail) (he : s(v, w) c.edges) (hw : w (c.takeUntil v ).support) :
theorem SimpleGraph.adj_and_reachable_delete_edges_iff_exists_cycle {V : Type u} {G : } {v : V} {w : V} :
G.Adj v w (G \ SimpleGraph.fromEdgeSet {s(v, w)}).Reachable