Traversing walks

Functions that help access different parts of a walk.

Main definitions

• SimpleGraph.Walk.getVert: Get the nth vertex encountered in a walk, or the last one if n is too large
• SimpleGraph.Walk.snd: The second vertex of a walk, or the only vertex in an empty walk
• SimpleGraph.Walk.penultimate: The penultimate vertex of a walk, or the only vertex in an empty walk
• SimpleGraph.Walk.firstDart: The first dart of a non-empty walk
• SimpleGraph.Walk.lastDart: The last dart of a non-empty walk

Tags

walks

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.

@[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 : ℕ} : 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) : (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) : (cons h p).getVert n = p.getVert (n - 1)

@[simp]

theorem SimpleGraph.Walk.getVert_mem_support {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (i : ℕ) : p.getVert i ∈ p.support

@[irreducible]

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

Use support_getElem_eq_getVert to rewrite in the reverse direction.

theorem SimpleGraph.Walk.support_getElem_eq_getVert {V : Type u} {G : SimpleGraph V} {u v : V} {n : ℕ} (p : G.Walk u v) (h : n < p.support.length) : p.support[n] = p.getVert n

Use getVert_eq_support_getElem to rewrite in the reverse direction.

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

theorem SimpleGraph.Walk.getVert_eq_getD_support {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (n : ℕ) : p.getVert n = p.support.getD n v

@[simp]

theorem SimpleGraph.Walk.getVert_support_idxOf {V : Type u} {G : SimpleGraph V} {u v w : V} [DecidableEq V] (p : G.Walk u v) (h : w ∈ p.support) : p.getVert (List.idxOf w p.support) = w

theorem SimpleGraph.Walk.getVert_comp_val_eq_get_support {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.getVert ∘ Fin.val = p.support.get

theorem SimpleGraph.Walk.range_getVert_eq_range_support_getElem {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : Set.range p.getVert = Set.range p.support.get

theorem SimpleGraph.Walk.darts_getElem_eq_getVert {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (n : ℕ) (h : n < p.darts.length) : p.darts[n] = { fst := p.getVert n, snd := p.getVert (n + 1), adj := ⋯ }

theorem SimpleGraph.Walk.adj_of_infix_support {V : Type u} {G : SimpleGraph V} {u v u' v' : V} {p : G.Walk u v} (h : [u', v'] <:+: p.support) : G.Adj u' v'

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

@[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) : (cons hadj q).snd = v

theorem SimpleGraph.Walk.snd_mem_tail_support {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (h : ¬p.Nil) : p.snd ∈ p.support.tail

@[simp]

theorem SimpleGraph.Walk.support_getElem_one {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (hp : 1 < p.support.length) : p.support[1] = p.snd

Use snd_eq_support_getElem_one to rewrite in the reverse direction.

theorem SimpleGraph.Walk.snd_eq_support_getElem_one {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (hnil : ¬p.Nil) : p.snd = p.support[1]

Use support_getElem_one to rewrite in the reverse direction.

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

@[simp]

theorem SimpleGraph.Walk.penultimate_nil {V : Type u} {G : SimpleGraph V} {v : V} : nil.penultimate = v

@[simp]

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

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

theorem SimpleGraph.Walk.penultimate_mem_dropLast_support {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (h : ¬p.Nil) : p.penultimate ∈ p.support.dropLast

@[simp]

theorem SimpleGraph.Walk.support_getElem_length_sub_one_eq_penultimate {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} : p.support[p.length - 1] = p.penultimate

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.

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

@[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.firstDart_eq {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} (h₁ : ¬p.Nil) (h₂ : 0 < p.darts.length) : p.firstDart h₁ = p.darts[0]

theorem SimpleGraph.Walk.lastDart_eq {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} (h₁ : ¬p.Nil) (h₂ : 0 < p.darts.length) : p.lastDart h₁ = p.darts[p.darts.length - 1]

@[simp]

theorem SimpleGraph.Walk.head_darts_eq_firstDart {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} (hnil : p.darts ≠ []) : p.darts.head hnil = p.firstDart ⋯

Use firstDart_eq_head_darts to rewrite in the reverse direction.

theorem SimpleGraph.Walk.firstDart_eq_head_darts {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} (hnil : ¬p.Nil) : p.firstDart hnil = p.darts.head ⋯

Use head_darts_eq_firstDart to rewrite in the reverse direction.

@[deprecated "Use `head_darts_eq_firstDart`" (since := "2025-12-10")]

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.firstDart_mem_darts {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} (hnil : ¬p.Nil) : p.firstDart hnil ∈ p.darts

@[simp]

theorem SimpleGraph.Walk.getLast_darts_eq_lastDart {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} (hnil : p.darts ≠ []) : p.darts.getLast hnil = p.lastDart ⋯

theorem SimpleGraph.Walk.lastDart_eq_getLast_darts {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} (hnil : ¬p.Nil) : p.lastDart hnil = p.darts.getLast ⋯

@[deprecated "Use `getLast_darts_eq_lastDart`" (since := "2025-12-10")]

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.lastDart_mem_darts {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} (hnil : ¬p.Nil) : p.lastDart hnil ∈ p.darts

@[simp]

theorem SimpleGraph.Walk.head_edges_eq_mk_start_snd {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} (hp : p.edges ≠ []) : p.edges.head hp = s(v, p.snd)

Use mk_start_snd_eq_head_edges to rewrite in the reverse direction.

theorem SimpleGraph.Walk.mk_start_snd_eq_head_edges {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} (hnil : ¬p.Nil) : s(v, p.snd) = p.edges.head ⋯

Use head_edges_eq_mk_start_snd to rewrite in the reverse direction.

theorem SimpleGraph.Walk.mk_start_snd_mem_edges {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} (hnil : ¬p.Nil) : s(v, p.snd) ∈ p.edges

@[simp]

theorem SimpleGraph.Walk.getLast_edges_eq_mk_penultimate_end {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} (hp : p.edges ≠ []) : p.edges.getLast hp = s(p.penultimate, w)

Use mk_penultimate_end_eq_getLast_edges to rewrite in the reverse direction.

theorem SimpleGraph.Walk.mk_penultimate_end_eq_getLast_edges {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} (hnil : ¬p.Nil) : s(p.penultimate, w) = p.edges.getLast ⋯

Use getLast_edges_eq_mk_penultimate_end to rewrite in the reverse direction.

theorem SimpleGraph.Walk.mk_penultimate_end_mem_edges {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} (hnil : ¬p.Nil) : s(p.penultimate, w) ∈ p.edges