Operations on walks

Operations on walks that produce a new walk in the same graph.

Main definitions

• SimpleGraph.Walk.copy: Change the endpoints of a walk using equalities
• SimpleGraph.Walk.append: Concatenate two compatible walks
• SimpleGraph.Walk.concat: Concatenate an edge to the end of a walk
• SimpleGraph.Walk.reverse: Reverse a walk
• SimpleGraph.Walk.drop: Remove the first n darts of a walk
• SimpleGraph.Walk.take: Take the first n darts of a walk
• SimpleGraph.Walk.tail: Remove the first dart of a walk
• SimpleGraph.Walk.dropLast: Remove the last dart of a walk

Tags

walks

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') : nil.copy hu hu = 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') : (cons h p).copy hu hw = 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) : cons h (p.copy hv hw) = (cons ⋯ p).copy ⋯ hw

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 (cons h 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

@[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) : (cons h p).append q = 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) : (cons h nil).append p = cons h p

@[simp]

theorem SimpleGraph.Walk.nil_append {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : 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 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) : nil.concat h = cons h 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) : (cons h p).concat h' = 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 (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), 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 = 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} : nil.reverse = nil

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

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

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

@[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.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 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 p) = ⋯ ▸ Hconcat p.reverse ⋯ (SimpleGraph.Walk.concatRecAux Hnil Hconcat p)

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 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 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) : concatRec Hnil Hconcat 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 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) : concatRec Hnil Hconcat (p.concat h) = Hconcat p h (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 ≠ 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'

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

theorem SimpleGraph.Walk.support_append_eq_support_dropLast_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.dropLast ++ p'.support

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_concat {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.support = p.support.dropLast.concat 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.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

theorem SimpleGraph.Walk.support_subset_support_concat {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v) (hadj : G.Adj v w) : p.support ⊆ (p.concat hadj).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.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}

@[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 { fst := v, snd := 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 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

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

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.mem_support_of_mem_edges {V : Type u} {G : SimpleGraph V} {u v w : V} {e : Sym2 V} {p : G.Walk u v} (he : e ∈ p.edges) (hv : w ∈ e) : w ∈ p.support

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

@[simp]

theorem SimpleGraph.Walk.edgeSet_reverse {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.reverse.edgeSet = p.edgeSet

@[simp]

theorem SimpleGraph.Walk.edgeSet_concat {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v) (h : G.Adj v w) : (p.concat h).edgeSet = insert s(v, w) p.edgeSet

theorem SimpleGraph.Walk.edgeSet_append {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v) (q : G.Walk v w) : (p.append q).edgeSet = p.edgeSet ∪ q.edgeSet

@[simp]

theorem SimpleGraph.Walk.edgeSet_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).edgeSet = p.edgeSet

@[simp]

theorem SimpleGraph.Walk.nil_append_iff {V : Type u} {G : SimpleGraph V} {u v w : V} {p : G.Walk u v} {q : G.Walk v w} : (p.append q).Nil ↔ p.Nil ∧ q.Nil

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

@[simp]

theorem SimpleGraph.Walk.nil_reverse {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} : p.reverse.Nil ↔ p.Nil

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

@[simp]

theorem SimpleGraph.Walk.drop_length {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (n : ℕ) : (p.drop n).length = p.length - n

@[simp]

theorem SimpleGraph.Walk.drop_getVert {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (n m : ℕ) : (p.drop n).getVert m = p.getVert (n + m)

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

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

Equations

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

@[simp]

theorem SimpleGraph.Walk.take_length {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (n : ℕ) : (p.take n).length = min n p.length

@[simp]

theorem SimpleGraph.Walk.take_getVert {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (n m : ℕ) : (p.take n).getVert m = p.getVert (min n m)

theorem SimpleGraph.Walk.take_support_eq_support_take_succ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (n : ℕ) : (p.take n).support = List.take (n + 1) p.support

@[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.snd_reverse {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.reverse.snd = p.penultimate

@[simp]

theorem SimpleGraph.Walk.penultimate_reverse {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.reverse.penultimate = p.snd

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

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

theorem SimpleGraph.Walk.drop_support_eq_support_drop_min {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (n : ℕ) : (p.drop n).support = List.drop (min n p.length) p.support

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

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

Equations

• p.dropLast = p.take (p.length - 1)

@[simp]

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

@[simp]

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

@[simp]

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

@[deprecated SimpleGraph.Walk.tail_cons (since := "2025-08-19")]

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) : (cons h p).tail = p.copy ⋯ ⋯

Alias of SimpleGraph.Walk.tail_cons.

@[simp]

theorem SimpleGraph.Walk.dropLast_nil {V : Type u} {G : SimpleGraph V} {v : V} : nil.dropLast = nil

@[simp]

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

@[simp]

theorem SimpleGraph.Walk.dropLast_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)).dropLast = cons h (cons h₂ p).dropLast

theorem SimpleGraph.Walk.dropLast_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).dropLast = cons h (p.dropLast.copy ⋯ ⋯)

@[simp]

theorem SimpleGraph.Walk.dropLast_concat {V : Type u} {G : SimpleGraph V} {t u v : V} (p : G.Walk u v) (h : G.Adj v t) : (p.concat h).dropLast = p.copy ⋯ ⋯

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

@[simp]

theorem SimpleGraph.Walk.concat_dropLast {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (hp : G.Adj p.penultimate v) : p.dropLast.concat hp = p

@[simp]

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

@[simp]

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

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

@[deprecated SimpleGraph.Walk.support_tail_of_not_nil (since := "2025-08-26")]

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

Alias of SimpleGraph.Walk.support_tail_of_not_nil.

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

theorem SimpleGraph.Walk.getVert_mem_tail_support {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (hp : ¬p.Nil) {i : ℕ} : i ≠ 0 → p.getVert i ∈ p.support.tail

theorem SimpleGraph.Walk.ext_support {V : Type u} {G : SimpleGraph V} {u v : V} {p q : G.Walk u v} (h : p.support = q.support) : p = q

theorem SimpleGraph.Walk.support_injective {V : Type u} {G : SimpleGraph V} {u v : V} : Function.Injective support

theorem SimpleGraph.Walk.ext_getVert_le_length {V : Type u} {G : SimpleGraph V} {u v : V} {p q : G.Walk u v} (hl : p.length = q.length) (h : ∀ k ≤ p.length, p.getVert k = q.getVert k) : p = q

theorem SimpleGraph.Walk.ext_getVert {V : Type u} {G : SimpleGraph V} {u v : V} {p q : G.Walk u v} (h : ∀ (k : ℕ), p.getVert k = q.getVert k) : p = q