Walk

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.

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.map for the induced map on walks, given an (injective) graph homomorphism.

Tags

walks

inductive SimpleGraph.Walk {V : Type u} (G : SimpleGraph V) : V → V → Type 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 : SimpleGraph V} {u : V} : G.Walk u u
• cons {V : Type u} {G : SimpleGraph V} {u v w : V} (h : G.Adj u v) (p : G.Walk v w) : G.Walk u w

instance SimpleGraph.instDecidableEqWalk {V✝ : Type u_1} {G✝ : SimpleGraph V✝} {a✝ a✝¹ : V✝} [DecidableEq V✝] : DecidableEq (G✝.Walk a✝ a✝¹)

Equations

• SimpleGraph.instDecidableEqWalk = SimpleGraph.decEqWalk✝

instance SimpleGraph.Walk.instInhabited {V : Type u} (G : SimpleGraph V) (v : V) : Inhabited (G.Walk v v)

Equations

• SimpleGraph.Walk.instInhabited G v = { default := SimpleGraph.Walk.nil }

@[simp]

theorem SimpleGraph.Walk.instInhabited_default {V : Type u} (G : SimpleGraph V) (v : V) : default = SimpleGraph.Walk.nil

@[reducible, match_pattern]

def SimpleGraph.Adj.toWalk {V : Type u} {G : SimpleGraph V} {u v : V} (h : G.Adj u v) : G.Walk u v

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

Equations

• h.toWalk = SimpleGraph.Walk.cons h SimpleGraph.Walk.nil

@[reducible, match_pattern, inline]

abbrev SimpleGraph.Walk.nil' {V : Type u} {G : SimpleGraph V} (u : V) : G.Walk u u

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

Equations

• SimpleGraph.Walk.nil' u = SimpleGraph.Walk.nil

@[reducible, match_pattern, inline]

abbrev SimpleGraph.Walk.cons' {V : Type u} {G : SimpleGraph V} (u 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

• SimpleGraph.Walk.cons' u v w h p = SimpleGraph.Walk.cons h p

def SimpleGraph.Walk.copy {V : Type u} {G : SimpleGraph V} {u v u' 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 = hu ▸ hv ▸ p

@[simp]

theorem SimpleGraph.Walk.copy_rfl_rfl {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.copy ⋯ ⋯ = p

@[simp]

theorem SimpleGraph.Walk.copy_copy {V : Type u} {G : SimpleGraph V} {u v u' v' u'' 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 : SimpleGraph V} {u u' : V} (hu : u = u') : SimpleGraph.Walk.nil.copy hu hu = SimpleGraph.Walk.nil

theorem SimpleGraph.Walk.copy_cons {V : Type u} {G : SimpleGraph V} {u v w u' w' : V} (h : G.Adj u v) (p : G.Walk v w) (hu : u = u') (hw : w = w') : (SimpleGraph.Walk.cons h p).copy hu hw = SimpleGraph.Walk.cons ⋯ (p.copy ⋯ hw)

@[simp]

theorem SimpleGraph.Walk.cons_copy {V : Type u} {G : SimpleGraph V} {u v w 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) = (SimpleGraph.Walk.cons ⋯ p).copy ⋯ hw

theorem SimpleGraph.Walk.exists_eq_cons_of_ne {V : Type u} {G : SimpleGraph 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 = SimpleGraph.Walk.cons h p'

def SimpleGraph.Walk.length {V : Type u} {G : SimpleGraph V} {u 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
• (SimpleGraph.Walk.cons h q).length = q.length.succ

def SimpleGraph.Walk.append {V : Type u} {G : SimpleGraph V} {u v w : V} : G.Walk u v → G.Walk v w → G.Walk u w

The concatenation of two compatible walks.

Equations

• SimpleGraph.Walk.nil.append q = q
• (SimpleGraph.Walk.cons h p).append x✝ = SimpleGraph.Walk.cons h (p.append x✝)

def SimpleGraph.Walk.concat {V : Type u} {G : SimpleGraph V} {u 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

• p.concat h = p.append (SimpleGraph.Walk.cons h SimpleGraph.Walk.nil)

theorem SimpleGraph.Walk.concat_eq_append {V : Type u} {G : SimpleGraph V} {u 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 : SimpleGraph 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

• SimpleGraph.Walk.nil.reverseAux x✝ = x✝
• (SimpleGraph.Walk.cons h p).reverseAux x✝ = p.reverseAux (SimpleGraph.Walk.cons ⋯ x✝)

def SimpleGraph.Walk.reverse {V : Type u} {G : SimpleGraph V} {u v : V} (w : G.Walk u v) : G.Walk v u

The walk in reverse.

Equations

• w.reverse = w.reverseAux SimpleGraph.Walk.nil

def SimpleGraph.Walk.getVert {V : Type u} {G : SimpleGraph V} {u v : V} : G.Walk u v → ℕ → V

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
• (SimpleGraph.Walk.cons h p).getVert 0 = u
• (SimpleGraph.Walk.cons h q).getVert n.succ = q.getVert n

@[simp]

theorem SimpleGraph.Walk.getVert_zero {V : Type u} {G : SimpleGraph V} {u v : V} (w : G.Walk u v) : w.getVert 0 = u

@[simp]

theorem SimpleGraph.Walk.getVert_nil {V : Type u} {G : SimpleGraph V} (u : V) {i : ℕ} : SimpleGraph.Walk.nil.getVert i = u

theorem SimpleGraph.Walk.getVert_of_length_le {V : Type u} {G : SimpleGraph V} {u 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 : SimpleGraph V} {u v : V} (w : G.Walk u v) : w.getVert w.length = v

theorem SimpleGraph.Walk.adj_getVert_succ {V : Type u} {G : SimpleGraph V} {u 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.getVert_cons_succ {V : Type u} {G : SimpleGraph V} {u v w : V} {n : ℕ} (p : G.Walk v w) (h : G.Adj u v) : (SimpleGraph.Walk.cons h p).getVert (n + 1) = p.getVert n

theorem SimpleGraph.Walk.getVert_cons {V : Type u} {G : SimpleGraph V} {u v w : V} {n : ℕ} (p : G.Walk v w) (h : G.Adj u v) (hn : n ≠ 0) : (SimpleGraph.Walk.cons h p).getVert n = p.getVert (n - 1)

@[simp]

theorem SimpleGraph.Walk.cons_append {V : Type u} {G : SimpleGraph V} {u v w x : V} (h : G.Adj u v) (p : G.Walk v w) (q : G.Walk w x) : (SimpleGraph.Walk.cons h p).append q = SimpleGraph.Walk.cons h (p.append q)

@[simp]

theorem SimpleGraph.Walk.cons_nil_append {V : Type u} {G : SimpleGraph V} {u v w : V} (h : G.Adj u v) (p : G.Walk v w) : (SimpleGraph.Walk.cons h SimpleGraph.Walk.nil).append p = SimpleGraph.Walk.cons h p

@[simp]

theorem SimpleGraph.Walk.nil_append {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : SimpleGraph.Walk.nil.append p = p

@[simp]

theorem SimpleGraph.Walk.append_nil {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.append SimpleGraph.Walk.nil = p

theorem SimpleGraph.Walk.append_assoc {V : Type u} {G : SimpleGraph 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

@[simp]

theorem SimpleGraph.Walk.append_copy_copy {V : Type u} {G : SimpleGraph V} {u v w u' 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 : SimpleGraph V} {u 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 : SimpleGraph V} {u v w x : V} (h : G.Adj u v) (p : G.Walk v w) (h' : G.Adj w x) : (SimpleGraph.Walk.cons h p).concat h' = SimpleGraph.Walk.cons h (p.concat h')

theorem SimpleGraph.Walk.append_concat {V : Type u} {G : SimpleGraph V} {u v w 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 : SimpleGraph V} {u v w x : V} (p : G.Walk u v) (h : G.Adj v w) (q : G.Walk w x) : (p.concat h).append q = p.append (SimpleGraph.Walk.cons h q)

theorem SimpleGraph.Walk.exists_cons_eq_concat {V : Type u} {G : SimpleGraph V} {u 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), SimpleGraph.Walk.cons h p = 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 : SimpleGraph V} {u 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 = SimpleGraph.Walk.cons h' q

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

@[simp]

theorem SimpleGraph.Walk.reverse_nil {V : Type u} {G : SimpleGraph V} {u : V} : SimpleGraph.Walk.nil.reverse = SimpleGraph.Walk.nil

theorem SimpleGraph.Walk.reverse_singleton {V : Type u} {G : SimpleGraph V} {u 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 : SimpleGraph V} {u v w x : V} (p : G.Walk u v) (q : G.Walk w x) (h : G.Adj w u) : (SimpleGraph.Walk.cons h p).reverseAux q = p.reverseAux (SimpleGraph.Walk.cons ⋯ q)

@[simp]

theorem SimpleGraph.Walk.append_reverseAux {V : Type u} {G : SimpleGraph V} {u v w 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 : SimpleGraph V} {u v w 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 : SimpleGraph V} {u 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 : SimpleGraph V} {u v w : V} (h : G.Adj u v) (p : G.Walk v w) : (SimpleGraph.Walk.cons h p).reverse = p.reverse.append (SimpleGraph.Walk.cons ⋯ SimpleGraph.Walk.nil)

@[simp]

theorem SimpleGraph.Walk.reverse_copy {V : Type u} {G : SimpleGraph V} {u v u' 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 : SimpleGraph V} {u 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 : SimpleGraph V} {u 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 : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.reverse.reverse = p

theorem SimpleGraph.Walk.reverse_surjective {V : Type u} {G : SimpleGraph V} {u v : V} : Function.Surjective SimpleGraph.Walk.reverse

theorem SimpleGraph.Walk.reverse_injective {V : Type u} {G : SimpleGraph V} {u v : V} : Function.Injective SimpleGraph.Walk.reverse

theorem SimpleGraph.Walk.reverse_bijective {V : Type u} {G : SimpleGraph V} {u v : V} : Function.Bijective SimpleGraph.Walk.reverse

@[simp]

theorem SimpleGraph.Walk.length_nil {V : Type u} {G : SimpleGraph V} {u : V} : SimpleGraph.Walk.nil.length = 0

@[simp]

theorem SimpleGraph.Walk.length_cons {V : Type u} {G : SimpleGraph V} {u v w : V} (h : G.Adj u v) (p : G.Walk v w) : (SimpleGraph.Walk.cons h p).length = p.length + 1

@[simp]

theorem SimpleGraph.Walk.length_copy {V : Type u} {G : SimpleGraph V} {u v u' 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 : SimpleGraph V} {u 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 : SimpleGraph V} {u 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 : SimpleGraph V} {u 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 : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.reverse.length = p.length

theorem SimpleGraph.Walk.eq_of_length_eq_zero {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} : p.length = 0 → u = v

theorem SimpleGraph.Walk.adj_of_length_eq_one {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} : p.length = 1 → G.Adj u v

@[simp]

theorem SimpleGraph.Walk.exists_length_eq_zero_iff {V : Type u} {G : SimpleGraph V} {u v : V} : (∃ (p : G.Walk u v), p.length = 0) ↔ u = v

@[simp]

theorem SimpleGraph.Walk.length_eq_zero_iff {V : Type u} {G : SimpleGraph V} {u : V} {p : G.Walk u u} : p.length = 0 ↔ p = SimpleGraph.Walk.nil

theorem SimpleGraph.Walk.getVert_append {V : Type u} {G : SimpleGraph V} {u 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 : SimpleGraph V} {u 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 : SimpleGraph V} {motive : (u v : V) → G.Walk u v → Sort 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 p → motive u w (p.concat h)) {u v : V} (p : G.Walk u v) : motive v u p.reverse

Auxiliary definition for SimpleGraph.Walk.concatRec

Equations

• SimpleGraph.Walk.concatRecAux Hnil Hconcat SimpleGraph.Walk.nil = Hnil
• SimpleGraph.Walk.concatRecAux Hnil Hconcat (SimpleGraph.Walk.cons h q) = ⋯ ▸ Hconcat q.reverse ⋯ (SimpleGraph.Walk.concatRecAux Hnil Hconcat q)

def SimpleGraph.Walk.concatRec {V : Type u} {G : SimpleGraph V} {motive : (u v : V) → G.Walk u v → Sort 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 p → motive u w (p.concat h)) {u 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

• SimpleGraph.Walk.concatRec Hnil Hconcat p = ⋯ ▸ SimpleGraph.Walk.concatRecAux Hnil Hconcat p.reverse

@[simp]

theorem SimpleGraph.Walk.concatRec_nil {V : Type u} {G : SimpleGraph V} {motive : (u v : V) → G.Walk u v → Sort 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 p → motive 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 : SimpleGraph V} {motive : (u v : V) → G.Walk u v → Sort 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 p → motive u w (p.concat h)) {u 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 : SimpleGraph V} {u 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 : SimpleGraph V} {u 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 : SimpleGraph 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

• SimpleGraph.Walk.nil.support = [u]
• (SimpleGraph.Walk.cons h q).support = u :: q.support

def SimpleGraph.Walk.darts {V : Type u} {G : SimpleGraph V} {u v : V} : G.Walk u v → List G.Dart

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

Equations

• SimpleGraph.Walk.nil.darts = []
• (SimpleGraph.Walk.cons h q).darts = { toProd := (u, v_3), adj := h } :: q.darts

def SimpleGraph.Walk.edges {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : List (Sym2 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

@[simp]

theorem SimpleGraph.Walk.support_nil {V : Type u} {G : SimpleGraph V} {u : V} : SimpleGraph.Walk.nil.support = [u]

@[simp]

theorem SimpleGraph.Walk.support_cons {V : Type u} {G : SimpleGraph V} {u v w : V} (h : G.Adj u v) (p : G.Walk v w) : (SimpleGraph.Walk.cons h p).support = u :: p.support

@[simp]

theorem SimpleGraph.Walk.support_concat {V : Type u} {G : SimpleGraph V} {u 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 : SimpleGraph V} {u v u' 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 : SimpleGraph V} {u 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 : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.reverse.support = p.support.reverse

@[simp]

theorem SimpleGraph.Walk.support_ne_nil {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.support ≠ []

@[simp]

theorem SimpleGraph.Walk.head_support {V : Type u} {G : SimpleGraph V} {a b : V} (p : G.Walk a b) : p.support.head ⋯ = a

@[simp]

theorem SimpleGraph.Walk.getLast_support {V : Type u} {G : SimpleGraph V} {a b : V} (p : G.Walk a b) : p.support.getLast ⋯ = b

theorem SimpleGraph.Walk.tail_support_append {V : Type u} {G : SimpleGraph 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

theorem SimpleGraph.Walk.support_eq_cons {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.support = u :: p.support.tail

@[simp]

theorem SimpleGraph.Walk.start_mem_support {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : u ∈ p.support

@[simp]

theorem SimpleGraph.Walk.end_mem_support {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : v ∈ p.support

@[simp]

theorem SimpleGraph.Walk.support_nonempty {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : {w : V | w ∈ p.support}.Nonempty

theorem SimpleGraph.Walk.mem_support_iff {V : Type u} {G : SimpleGraph V} {u 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 : SimpleGraph V} {u v : V} : u ∈ SimpleGraph.Walk.nil.support ↔ u = v

@[simp]

theorem SimpleGraph.Walk.mem_tail_support_append_iff {V : Type u} {G : SimpleGraph 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

@[simp]

theorem SimpleGraph.Walk.end_mem_tail_support_of_ne {V : Type u} {G : SimpleGraph V} {u 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 : SimpleGraph 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

@[simp]

theorem SimpleGraph.Walk.subset_support_append_left {V : Type u} {G : SimpleGraph V} {u 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 : SimpleGraph V} {u v w : V} (p : G.Walk u v) (q : G.Walk v w) : q.support ⊆ (p.append q).support

theorem SimpleGraph.Walk.getVert_eq_support_get? {V : Type u} {G : SimpleGraph V} {u v : V} {n : ℕ} (p : G.Walk u v) (h2 : n ≤ p.length) : some (p.getVert n) = p.support[n]?

theorem SimpleGraph.Walk.coe_support {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : ↑p.support = {u} + ↑p.support.tail

theorem SimpleGraph.Walk.coe_support_append {V : Type u} {G : SimpleGraph 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

theorem SimpleGraph.Walk.coe_support_append' {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u 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 : SimpleGraph V} {u 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 : SimpleGraph V} {u v : V} (p : G.Walk u v) : List.Chain' G.Adj p.support

theorem SimpleGraph.Walk.chain_dartAdj_darts {V : Type u} {G : SimpleGraph V} {d : G.Dart} {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 : SimpleGraph V} {u v : V} (p : G.Walk u v) : List.Chain' G.DartAdj p.darts

theorem SimpleGraph.Walk.edges_subset_edgeSet {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) ⦃e : Sym2 V⦄ : e ∈ p.edges → e ∈ 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 : SimpleGraph V} {u v x y : V} (p : G.Walk u v) (h : s(x, y) ∈ p.edges) : G.Adj x y

@[simp]

theorem SimpleGraph.Walk.darts_nil {V : Type u} {G : SimpleGraph V} {u : V} : SimpleGraph.Walk.nil.darts = []

@[simp]

theorem SimpleGraph.Walk.darts_cons {V : Type u} {G : SimpleGraph V} {u v w : V} (h : G.Adj u v) (p : G.Walk v w) : (SimpleGraph.Walk.cons h p).darts = { toProd := (u, v), adj := h } :: p.darts

@[simp]

theorem SimpleGraph.Walk.darts_concat {V : Type u} {G : SimpleGraph V} {u 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 : SimpleGraph V} {u v u' 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 : SimpleGraph V} {u 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 : SimpleGraph V} {u 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 : SimpleGraph V} {u 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 : SimpleGraph V} {u 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 : SimpleGraph V} {u 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 : SimpleGraph V} {u 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 : SimpleGraph V} {u 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.head_darts_fst {V : Type u} {G : SimpleGraph V} {a b : V} (p : G.Walk a b) (hp : p.darts ≠ []) : (p.darts.head hp).toProd.1 = a

@[simp]

theorem SimpleGraph.Walk.getLast_darts_snd {V : Type u} {G : SimpleGraph V} {a b : V} (p : G.Walk a b) (hp : p.darts ≠ []) : (p.darts.getLast hp).toProd.2 = b

@[simp]

theorem SimpleGraph.Walk.edges_nil {V : Type u} {G : SimpleGraph V} {u : V} : SimpleGraph.Walk.nil.edges = []

@[simp]

theorem SimpleGraph.Walk.edges_cons {V : Type u} {G : SimpleGraph V} {u v w : V} (h : G.Adj u v) (p : G.Walk v w) : (SimpleGraph.Walk.cons h p).edges = s(u, v) :: p.edges

@[simp]

theorem SimpleGraph.Walk.edges_concat {V : Type u} {G : SimpleGraph V} {u 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 : SimpleGraph V} {u v u' 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 : SimpleGraph V} {u 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 : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.reverse.edges = p.edges.reverse

@[simp]

theorem SimpleGraph.Walk.length_support {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.support.length = p.length + 1

@[simp]

theorem SimpleGraph.Walk.length_darts {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.darts.length = p.length

@[simp]

theorem SimpleGraph.Walk.length_edges {V : Type u} {G : SimpleGraph V} {u 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 : SimpleGraph V} {u v : V} (p : G.Walk u v) {d : G.Dart} : d ∈ p.darts → d.toProd.1 ∈ p.support

theorem SimpleGraph.Walk.dart_snd_mem_support_of_mem_darts {V : Type u} {G : SimpleGraph V} {u 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 : SimpleGraph V} {t u 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 : SimpleGraph V} {t u 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 : SimpleGraph V} {u 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 : SimpleGraph V} {u v : V} {p : G.Walk u v} (h : p.support.Nodup) : p.edges.Nodup

theorem SimpleGraph.Walk.nodup_tail_support_reverse {V : Type u} {G : SimpleGraph V} {u : V} {p : G.Walk u u} : p.reverse.support.tail.Nodup ↔ p.support.tail.Nodup

theorem SimpleGraph.Walk.edges_injective {V : Type u} {G : SimpleGraph V} {u v : V} : Function.Injective SimpleGraph.Walk.edges

theorem SimpleGraph.Walk.darts_injective {V : Type u} {G : SimpleGraph V} {u v : V} : Function.Injective SimpleGraph.Walk.darts

inductive SimpleGraph.Walk.Nil {V : Type u} {G : SimpleGraph V} {v w : V} : G.Walk v w → Prop

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 : SimpleGraph V} {u : V} : SimpleGraph.Walk.nil.Nil

@[simp]

theorem SimpleGraph.Walk.nil_nil {V : Type u} {G : SimpleGraph V} {u : V} : SimpleGraph.Walk.nil.Nil

@[simp]

theorem SimpleGraph.Walk.not_nil_cons {V : Type u} {G : SimpleGraph V} {u v w : V} {h : G.Adj u v} {p : G.Walk v w} : ¬(SimpleGraph.Walk.cons h p).Nil

instance SimpleGraph.Walk.instDecidableNil {V : Type u} {G : SimpleGraph V} {v w : V} (p : G.Walk v w) : Decidable p.Nil

Equations

• SimpleGraph.Walk.nil.instDecidableNil = isTrue ⋯
• (SimpleGraph.Walk.cons h q).instDecidableNil = isFalse ⋯

theorem SimpleGraph.Walk.Nil.eq {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} : p.Nil → v = w

theorem SimpleGraph.Walk.not_nil_of_ne {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} : v ≠ w → ¬p.Nil

theorem SimpleGraph.Walk.nil_iff_support_eq {V : Type u} {G : SimpleGraph 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 : SimpleGraph V} {v w : V} {p : G.Walk v w} : p.Nil ↔ p.length = 0

theorem SimpleGraph.Walk.not_nil_iff_lt_length {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} : ¬p.Nil ↔ 0 < p.length

theorem SimpleGraph.Walk.not_nil_iff {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} : ¬p.Nil ↔ ∃ (u : V) (h : G.Adj v u) (q : G.Walk u w), p = SimpleGraph.Walk.cons h q

theorem SimpleGraph.Walk.nil_iff_eq_nil {V : Type u} {G : SimpleGraph V} {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 : SimpleGraph V} {v : V} {p : G.Walk v v} : p.Nil → p = 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 : SimpleGraph V} {u w : V} {motive : {u w : V} → (p : G.Walk u w) → ¬p.Nil → Sort u_1} (cons : {u v w : V} → (h : G.Adj u v) → (q : G.Walk v w) → motive (SimpleGraph.Walk.cons h q) ⋯) (p : G.Walk u w) (hp : ¬p.Nil) : motive p hp

Equations

• SimpleGraph.Walk.notNilRec cons SimpleGraph.Walk.nil = fun (hp : ¬SimpleGraph.Walk.nil.Nil) => absurd ⋯ hp
• SimpleGraph.Walk.notNilRec cons (SimpleGraph.Walk.cons h q) = fun (x : ¬(SimpleGraph.Walk.cons h q).Nil) => cons h q

@[simp]

theorem SimpleGraph.Walk.notNilRec_cons {V : Type u} {G : SimpleGraph V} {u v w : V} {motive : {u w : V} → (p : G.Walk u w) → ¬p.Nil → Sort u_1} (cons : {u v w : V} → (h : G.Adj u v) → (q : G.Walk v w) → motive (SimpleGraph.Walk.cons h q) ⋯) (h' : G.Adj u v) (q' : G.Walk v w) : SimpleGraph.Walk.notNilRec (fun {u v w : V} => cons) (SimpleGraph.Walk.cons h' q') ⋯ = cons h' q'

def SimpleGraph.Walk.drop {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (n : ℕ) : G.Walk (p.getVert n) v

The walk obtained by removing the first n darts of a walk.

Equations

• SimpleGraph.Walk.nil.drop n = SimpleGraph.Walk.nil
• p.drop 0 = p.copy ⋯ ⋯
• (SimpleGraph.Walk.cons h q).drop n_2.succ = (q.drop n_2).copy ⋯ ⋯

@[reducible, inline]

abbrev SimpleGraph.Walk.snd {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : V

The second vertex of a walk, or the only vertex in a nil walk.

Equations

• p.snd = p.getVert 1

@[simp]

theorem SimpleGraph.Walk.adj_snd {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} (hp : ¬p.Nil) : G.Adj v p.snd

theorem SimpleGraph.Walk.snd_cons {V : Type u} {G : SimpleGraph V} {u v w : V} (q : G.Walk v w) (hadj : G.Adj u v) : (SimpleGraph.Walk.cons hadj q).snd = v

@[reducible, inline]

abbrev SimpleGraph.Walk.penultimate {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : V

The penultimate vertex of a walk, or the only vertex in a nil walk.

Equations

• p.penultimate = p.getVert (p.length - 1)

@[simp]

theorem SimpleGraph.Walk.penultimate_cons_nil {V : Type u} {G : SimpleGraph V} {u v : V} (h : G.Adj u v) : (SimpleGraph.Walk.cons h SimpleGraph.Walk.nil).penultimate = u

@[simp]

theorem SimpleGraph.Walk.penultimate_cons_cons {V : Type u} {G : SimpleGraph V} {u v w w' : V} (h : G.Adj u v) (h₂ : G.Adj v w) (p : G.Walk w w') : (SimpleGraph.Walk.cons h (SimpleGraph.Walk.cons h₂ p)).penultimate = (SimpleGraph.Walk.cons h₂ p).penultimate

theorem SimpleGraph.Walk.penultimate_cons_of_not_nil {V : Type u} {G : SimpleGraph V} {u v w : V} (h : G.Adj u v) (p : G.Walk v w) (hp : ¬p.Nil) : (SimpleGraph.Walk.cons h p).penultimate = p.penultimate

@[simp]

theorem SimpleGraph.Walk.penultimate_concat {V : Type u} {G : SimpleGraph V} {t u v : V} (p : G.Walk u v) (h : G.Adj v t) : (p.concat h).penultimate = v

@[simp]

theorem SimpleGraph.Walk.adj_penultimate {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} (hp : ¬p.Nil) : G.Adj p.penultimate w

def SimpleGraph.Walk.tail {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : G.Walk p.snd v

The walk obtained by removing the first dart of a walk. A nil walk stays nil.

Equations

• p.tail = p.drop 1

@[simp]

theorem SimpleGraph.Walk.tail_nil {V : Type u} {G : SimpleGraph V} {v : V} : SimpleGraph.Walk.nil.tail = SimpleGraph.Walk.nil

@[simp]

theorem SimpleGraph.Walk.tail_cons_nil {V : Type u} {G : SimpleGraph V} {u v : V} (h : G.Adj u v) : (SimpleGraph.Walk.cons h SimpleGraph.Walk.nil).tail = SimpleGraph.Walk.nil

theorem SimpleGraph.Walk.tail_cons_eq {V : Type u} {G : SimpleGraph V} {u v w : V} (h : G.Adj u v) (p : G.Walk v w) : (SimpleGraph.Walk.cons h p).tail = p.copy ⋯ ⋯

def SimpleGraph.Walk.firstDart {V : Type u} {G : SimpleGraph 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.snd), adj := ⋯ }

@[simp]

theorem SimpleGraph.Walk.firstDart_toProd {V : Type u} {G : SimpleGraph V} {v w : V} (p : G.Walk v w) (hp : ¬p.Nil) : (p.firstDart hp).toProd = (v, p.snd)

def SimpleGraph.Walk.lastDart {V : Type u} {G : SimpleGraph V} {v w : V} (p : G.Walk v w) (hp : ¬p.Nil) : G.Dart

The last dart of a walk.

Equations

• p.lastDart hp = { toProd := (p.penultimate, w), adj := ⋯ }

@[simp]

theorem SimpleGraph.Walk.lastDart_toProd {V : Type u} {G : SimpleGraph V} {v w : V} (p : G.Walk v w) (hp : ¬p.Nil) : (p.lastDart hp).toProd = (p.penultimate, w)

theorem SimpleGraph.Walk.edge_firstDart {V : Type u} {G : SimpleGraph V} {v w : V} (p : G.Walk v w) (hp : ¬p.Nil) : (p.firstDart hp).edge = s(v, p.snd)

theorem SimpleGraph.Walk.edge_lastDart {V : Type u} {G : SimpleGraph V} {v w : V} (p : G.Walk v w) (hp : ¬p.Nil) : (p.lastDart hp).edge = s(p.penultimate, w)

theorem SimpleGraph.Walk.cons_tail_eq {V : Type u} {G : SimpleGraph V} {x y : V} (p : G.Walk x y) (hp : ¬p.Nil) : SimpleGraph.Walk.cons ⋯ p.tail = p

@[simp]

theorem SimpleGraph.Walk.cons_support_tail {V : Type u} {G : SimpleGraph V} {x y : V} (p : G.Walk x y) (hp : ¬p.Nil) : x :: p.tail.support = p.support

@[simp]

theorem SimpleGraph.Walk.length_tail_add_one {V : Type u} {G : SimpleGraph V} {x y : V} {p : G.Walk x y} (hp : ¬p.Nil) : p.tail.length + 1 = p.length

theorem SimpleGraph.Walk.Nil.tail {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} (hp : p.Nil) : p.tail.Nil

theorem SimpleGraph.Walk.not_nil_of_tail_not_nil {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} (hp : ¬p.tail.Nil) : ¬p.Nil

@[simp]

theorem SimpleGraph.Walk.nil_copy {V : Type u} {G : SimpleGraph V} {x y x' 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 : SimpleGraph V} {v : V} (p : G.Walk v v) (hp : ¬p.Nil) : p.tail.support = p.support.tail

@[simp]

theorem SimpleGraph.Walk.tail_cons {V : Type u} {G : SimpleGraph V} {t u v : V} (p : G.Walk u v) (h : G.Adj t u) : (SimpleGraph.Walk.cons h p).tail = p.copy ⋯ ⋯

theorem SimpleGraph.Walk.support_tail_of_not_nil {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (hnp : ¬p.Nil) : p.tail.support = p.support.tail

Walk decompositions

def SimpleGraph.Walk.takeUntil {V : Type u} {G : SimpleGraph V} [DecidableEq V] {v w : V} (p : G.Walk v w) (u : V) : u ∈ p.support → G.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

def SimpleGraph.Walk.dropUntil {V : Type u} {G : SimpleGraph V} [DecidableEq V] {v w : V} (p : G.Walk v w) (u : V) : u ∈ p.support → G.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

@[simp]

theorem SimpleGraph.Walk.take_spec {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u 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 : SimpleGraph V} {u 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 : SimpleGraph V} [DecidableEq V] {u 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 : SimpleGraph V} [DecidableEq V] {u 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 : SimpleGraph V} [DecidableEq V] {u v w 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 : SimpleGraph V} [DecidableEq V] {u v w 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 : SimpleGraph V} [DecidableEq V] {u 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 : SimpleGraph V} [DecidableEq V] {u 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 : SimpleGraph V} [DecidableEq V] {u 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 : SimpleGraph V} [DecidableEq V] {u 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 : SimpleGraph V} [DecidableEq V] {u 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 : SimpleGraph V} [DecidableEq V] {u 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 : SimpleGraph V} [DecidableEq V] {u 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 : SimpleGraph V} [DecidableEq V] {u v w : V} (p : G.Walk v w) (h : u ∈ p.support) : (p.dropUntil u h).length ≤ p.length

def SimpleGraph.Walk.rotate {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u 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)

@[simp]

theorem SimpleGraph.Walk.support_rotate {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u 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 : SimpleGraph V} [DecidableEq V] {u 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 : SimpleGraph V} [DecidableEq V] {u v : V} (c : G.Walk v v) (h : u ∈ c.support) : (c.rotate h).edges ~r c.edges

theorem SimpleGraph.Walk.exists_boundary_dart {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (S : Set V) (uS : u ∈ S) (vS : v ∉ S) : ∃ d ∈ p.darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S

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.

@[simp]

theorem SimpleGraph.Walk.getVert_copy {V : Type u} {G : SimpleGraph V} {u v w x : V} (p : G.Walk u v) (i : ℕ) (h : u = w) (h' : v = x) : (p.copy h h').getVert i = p.getVert i

@[simp]

theorem SimpleGraph.Walk.getVert_tail {V : Type u} {G : SimpleGraph V} {u v : V} {n : ℕ} (p : G.Walk u v) : p.tail.getVert n = p.getVert (n + 1)

@[irreducible]

theorem SimpleGraph.Walk.mem_support_iff_exists_getVert {V : Type u} {G : SimpleGraph V} {u v w : V} {p : G.Walk v w} : u ∈ p.support ↔ ∃ (n : ℕ), p.getVert n = u ∧ n ≤ p.length

Given a walk w and a node in the support, there exists a natural n, such that given node is the n-th node (zero-indexed) in the walk. In addition, n is at most the length of the path. Due to the definition of getVert it would otherwise be legal to return a larger n for the last node.

Mapping walks

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

Given a graph homomorphism, map walks to walks.

Equations

• SimpleGraph.Walk.map f SimpleGraph.Walk.nil = SimpleGraph.Walk.nil
• SimpleGraph.Walk.map f (SimpleGraph.Walk.cons h q) = SimpleGraph.Walk.cons ⋯ (SimpleGraph.Walk.map f q)

@[simp]

theorem SimpleGraph.Walk.map_nil {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (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 : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u v : V} (p : G.Walk u v) {w : V} (h : G.Adj w u) : SimpleGraph.Walk.map f (SimpleGraph.Walk.cons h p) = SimpleGraph.Walk.cons ⋯ (SimpleGraph.Walk.map f p)

@[simp]

theorem SimpleGraph.Walk.map_copy {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u v u' v' : V} (p : G.Walk u v) (hu : u = u') (hv : v = v') : SimpleGraph.Walk.map f (p.copy hu hv) = (SimpleGraph.Walk.map f p).copy ⋯ ⋯

@[simp]

theorem SimpleGraph.Walk.map_id {V : Type u} {G : SimpleGraph V} {u v : 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 : SimpleGraph V} {G' : SimpleGraph V'} {G'' : SimpleGraph V''} (f : G →g G') (f' : G' →g G'') {u v : V} (p : G.Walk u v) : SimpleGraph.Walk.map f' (SimpleGraph.Walk.map f p) = SimpleGraph.Walk.map (f'.comp f) p

theorem SimpleGraph.Walk.map_eq_of_eq {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {u v : V} (p : G.Walk u v) {f : G →g G'} (f' : G →g G') (h : f = f') : SimpleGraph.Walk.map f p = (SimpleGraph.Walk.map f' p).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 : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u : V} {p : G.Walk u u} : SimpleGraph.Walk.map f p = SimpleGraph.Walk.nil ↔ p = SimpleGraph.Walk.nil

@[simp]

theorem SimpleGraph.Walk.length_map {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u v : V} (p : G.Walk u v) : (SimpleGraph.Walk.map f p).length = p.length

theorem SimpleGraph.Walk.map_append {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u v w : V} (p : G.Walk u v) (q : G.Walk v w) : SimpleGraph.Walk.map f (p.append q) = (SimpleGraph.Walk.map f p).append (SimpleGraph.Walk.map f q)

@[simp]

theorem SimpleGraph.Walk.reverse_map {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u v : V} (p : G.Walk u v) : (SimpleGraph.Walk.map f p).reverse = SimpleGraph.Walk.map f p.reverse

@[simp]

theorem SimpleGraph.Walk.support_map {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u v : V} (p : G.Walk u v) : (SimpleGraph.Walk.map f p).support = List.map (⇑f) p.support

@[simp]

theorem SimpleGraph.Walk.darts_map {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u v : V} (p : G.Walk u v) : (SimpleGraph.Walk.map f p).darts = List.map f.mapDart p.darts

@[simp]

theorem SimpleGraph.Walk.edges_map {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u v : V} (p : G.Walk u v) : (SimpleGraph.Walk.map f p).edges = List.map (Sym2.map ⇑f) p.edges

theorem SimpleGraph.Walk.map_injective_of_injective {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G →g G'} (hinj : Function.Injective ⇑f) (u v : V) : Function.Injective (SimpleGraph.Walk.map f)

@[reducible, inline]

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

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

Equations

• SimpleGraph.Walk.mapLe h p = SimpleGraph.Walk.map (SimpleGraph.Hom.mapSpanningSubgraphs h) p

Transferring between graphs

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

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

Equations

• SimpleGraph.Walk.nil.transfer H h_2 = SimpleGraph.Walk.nil
• (SimpleGraph.Walk.cons h_2 p_2).transfer H h_3 = SimpleGraph.Walk.cons ⋯ (p_2.transfer H ⋯)

theorem SimpleGraph.Walk.transfer_self {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.transfer G ⋯ = p

theorem SimpleGraph.Walk.transfer_eq_map_of_le {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) {H : SimpleGraph V} (hp : ∀ e ∈ p.edges, e ∈ H.edgeSet) (GH : G ≤ H) : p.transfer H hp = SimpleGraph.Walk.map (SimpleGraph.Hom.mapSpanningSubgraphs GH) p

@[simp]

theorem SimpleGraph.Walk.edges_transfer {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) {H : SimpleGraph V} (hp : ∀ e ∈ p.edges, e ∈ H.edgeSet) : (p.transfer H hp).edges = p.edges

@[simp]

theorem SimpleGraph.Walk.support_transfer {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) {H : SimpleGraph V} (hp : ∀ e ∈ p.edges, e ∈ H.edgeSet) : (p.transfer H hp).support = p.support

@[simp]

theorem SimpleGraph.Walk.length_transfer {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) {H : SimpleGraph V} (hp : ∀ e ∈ p.edges, e ∈ H.edgeSet) : (p.transfer H hp).length = p.length

@[simp]

theorem SimpleGraph.Walk.transfer_transfer {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) {H : SimpleGraph V} (hp : ∀ e ∈ p.edges, e ∈ H.edgeSet) {K : SimpleGraph V} (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 : SimpleGraph V} {u v : V} (p : G.Walk u v) {H : SimpleGraph V} {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 : SimpleGraph V} {u v : V} (p : G.Walk u v) {H : SimpleGraph V} (hp : ∀ e ∈ p.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 : SimpleGraph V} (s : Set (Sym2 V)) {v w : V} (p : G.Walk v w) (hp : ∀ e ∈ p.edges, e ∉ s) : (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

• SimpleGraph.Walk.toDeleteEdges s p hp = p.transfer (G.deleteEdges s) ⋯

@[simp]

theorem SimpleGraph.Walk.toDeleteEdges_nil {V : Type u} {G : SimpleGraph V} (s : Set (Sym2 V)) {v : V} (hp : ∀ e ∈ SimpleGraph.Walk.nil.edges, e ∉ s) : SimpleGraph.Walk.toDeleteEdges s SimpleGraph.Walk.nil hp = SimpleGraph.Walk.nil

@[simp]

theorem SimpleGraph.Walk.toDeleteEdges_cons {V : Type u} {G : SimpleGraph V} (s : Set (Sym2 V)) {u v w : V} (h : G.Adj u v) (p : G.Walk v w) (hp : ∀ e ∈ (SimpleGraph.Walk.cons h p).edges, e ∉ s) : SimpleGraph.Walk.toDeleteEdges s (SimpleGraph.Walk.cons h p) hp = SimpleGraph.Walk.cons ⋯ (SimpleGraph.Walk.toDeleteEdges s p ⋯)

@[reducible, inline]

abbrev SimpleGraph.Walk.toDeleteEdge {V : Type u} {G : SimpleGraph V} {v w : V} (e : Sym2 V) (p : G.Walk v w) (hp : e ∉ p.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

• SimpleGraph.Walk.toDeleteEdge e p hp = SimpleGraph.Walk.toDeleteEdges {e} p ⋯

@[simp]

theorem SimpleGraph.Walk.map_toDeleteEdges_eq {V : Type u} {G : SimpleGraph V} {v w : V} (s : Set (Sym2 V)) {p : G.Walk v w} (hp : ∀ e ∈ p.edges, e ∉ s) : SimpleGraph.Walk.map (SimpleGraph.Hom.mapSpanningSubgraphs ⋯) (SimpleGraph.Walk.toDeleteEdges s p hp) = p