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.

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

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]?

@[deprecated SimpleGraph.Walk.getVert_eq_support_getElem? (since := "2025-06-10")]

theorem SimpleGraph.Walk.getVert_eq_support_get? {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]?

Alias of SimpleGraph.Walk.getVert_eq_support_getElem?.

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

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

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

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

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 = { fst := v, snd := 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 = { fst := p.penultimate, snd := 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.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]