Subwalks

We define a relation on walks stating that one walk is the subwalk of another.

Main definitions

• SimpleGraph.Walk.IsSubwalk: A relation on walks stating that the first walk is a contiguous subwalk of the second walk.

Tags

walks, subwalks

def SimpleGraph.Walk.IsSubwalk {V : Type u_1} {G : SimpleGraph V} {u₁ v₁ u₂ v₂ : V} (p : G.Walk u₁ v₁) (q : G.Walk u₂ v₂) : Prop

p.IsSubwalk q means that the walk p is a contiguous subwalk of the walk q.

@[simp]

theorem SimpleGraph.Walk.isSubwalk_rfl {V : Type u_1} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.IsSubwalk p

@[simp]

theorem SimpleGraph.Walk.isSubwalk_nil_start {V : Type u_1} {G : SimpleGraph V} {u v : V} (q : G.Walk u v) : nil.IsSubwalk q

@[deprecated SimpleGraph.Walk.isSubwalk_nil_start (since := "2026-07-11")]

theorem SimpleGraph.Walk.nil_isSubwalk {V : Type u_1} {G : SimpleGraph V} {u v : V} (q : G.Walk u v) : nil.IsSubwalk q

Alias of SimpleGraph.Walk.isSubwalk_nil_start.

@[simp]

theorem SimpleGraph.Walk.isSubwalk_nil_end {V : Type u_1} {G : SimpleGraph V} {u v : V} (q : G.Walk u v) : nil.IsSubwalk q

theorem SimpleGraph.Walk.IsSubwalk.cons {V : Type u_1} {G : SimpleGraph V} {u v u' v' w : V} {p : G.Walk u v} {q : G.Walk u' v'} (hpq : p.IsSubwalk q) (h : G.Adj w u') : p.IsSubwalk (cons h q)

@[simp]

theorem SimpleGraph.Walk.isSubwalk_cons {V : Type u_1} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v) (h : G.Adj w u) : p.IsSubwalk (cons h p)

theorem SimpleGraph.Walk.IsSubwalk.concat {V : Type u_1} {G : SimpleGraph V} {u v u' v' w : V} {p : G.Walk u v} {q : G.Walk u' v'} (hpq : p.IsSubwalk q) (h : G.Adj v' w) : p.IsSubwalk (q.concat h)

@[simp]

theorem SimpleGraph.Walk.isSubwalk_concat {V : Type u_1} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v) (h : G.Adj v w) : p.IsSubwalk (p.concat h)

theorem SimpleGraph.Walk.IsSubwalk.trans {V : Type u_1} {G : SimpleGraph V} {u₁ v₁ u₂ v₂ u₃ v₃ : V} {p₁ : G.Walk u₁ v₁} {p₂ : G.Walk u₂ v₂} {p₃ : G.Walk u₃ v₃} (h₁ : p₁.IsSubwalk p₂) (h₂ : p₂.IsSubwalk p₃) : p₁.IsSubwalk p₃

theorem SimpleGraph.Walk.isSubwalk_nil_iff {V : Type u_1} {G : SimpleGraph V} {u v u' : V} (p : G.Walk u v) : p.IsSubwalk nil ↔ ∃ (hu : u' = u) (hv : u' = v), p = nil.copy hu hv

theorem SimpleGraph.Walk.nil_isSubwalk_iff_exists {V : Type u_1} {G : SimpleGraph V} {u' u v : V} (q : G.Walk u v) : nil.IsSubwalk q ↔ ∃ (ru : G.Walk u u') (rv : G.Walk u' v), q = ru.append rv

theorem SimpleGraph.Walk.length_le_of_isSubwalk {V : Type u_1} {G : SimpleGraph V} {u₁ v₁ u₂ v₂ : V} {q : G.Walk u₁ v₁} {p : G.Walk u₂ v₂} (h : p.IsSubwalk q) : p.length ≤ q.length

theorem SimpleGraph.Walk.isSubwalk_of_append_left {V : Type u_1} {G : SimpleGraph V} {v w u : V} {p₁ : G.Walk v w} {p₂ : G.Walk w u} {p₃ : G.Walk v u} (h : p₃ = p₁.append p₂) : p₁.IsSubwalk p₃

theorem SimpleGraph.Walk.isSubwalk_of_append_right {V : Type u_1} {G : SimpleGraph V} {v w u : V} {p₁ : G.Walk v w} {p₂ : G.Walk w u} {p₃ : G.Walk v u} (h : p₃ = p₁.append p₂) : p₂.IsSubwalk p₃

theorem SimpleGraph.Walk.isSubwalk_take {V : Type u_1} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (n : ℕ) : (p.take n).IsSubwalk p

theorem SimpleGraph.Walk.isSubwalk_drop {V : Type u_1} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (n : ℕ) : (p.drop n).IsSubwalk p

theorem SimpleGraph.Walk.isSubwalk_iff_support_isInfix {V : Type u_1} {G : SimpleGraph V} {v w v' w' : V} {p₁ : G.Walk v w} {p₂ : G.Walk v' w'} : p₁.IsSubwalk p₂ ↔ p₁.support <:+: p₂.support

theorem SimpleGraph.Walk.isSubwalk_iff_darts_isInfix {V : Type u_1} {G : SimpleGraph V} {u v u' v' : V} {p₁ : G.Walk u v} {p₂ : G.Walk u' v'} (hnil : ¬p₁.Nil) : p₁.IsSubwalk p₂ ↔ p₁.darts <:+: p₂.darts

@[simp]

theorem SimpleGraph.Walk.isSubwalk_nil_iff_mem_support {V : Type u_1} {G : SimpleGraph V} {u v v' : V} (p : G.Walk u v) : nil.IsSubwalk p ↔ v' ∈ p.support

theorem SimpleGraph.Walk.isSubwalk_toWalk_iff_mem_darts {V : Type u_1} {G : SimpleGraph V} {u v u' v' : V} (p : G.Walk u v) (h : G.Adj u' v') : h.toWalk.IsSubwalk p ↔ { fst := u', snd := v', adj := h } ∈ p.darts

theorem SimpleGraph.Walk.isSubwalk_toWalk_adj_iff_mem_darts {V : Type u_1} {G : SimpleGraph V} {u v : V} {d : G.Dart} (p : G.Walk u v) : ⋯.toWalk.IsSubwalk p ↔ d ∈ p.darts

theorem SimpleGraph.Walk.isSubwalk_toWalk_iff_mem_edges {V : Type u_1} {G : SimpleGraph V} {u v u' v' : V} {p : G.Walk u v} (h : G.Adj u' v') : h.toWalk.IsSubwalk p ∨ ⋯.toWalk.IsSubwalk p ↔ s(u', v') ∈ p.edges

theorem SimpleGraph.Walk.infix_support_iff_mem_edges {V : Type u_1} {G : SimpleGraph V} {u v u' v' : V} {p : G.Walk u v} : [u', v'] <:+: p.support ∨ [v', u'] <:+: p.support ↔ s(u', v') ∈ p.edges

theorem SimpleGraph.Walk.isSubwalk_antisymm {V : Type u_1} {G : SimpleGraph V} {u v : V} {p₁ p₂ : G.Walk u v} (h₁ : p₁.IsSubwalk p₂) (h₂ : p₂.IsSubwalk p₁) : p₁ = p₂

@[simp]

theorem SimpleGraph.Walk.IsSubwalk.support_subset {V : Type u_1} {G : SimpleGraph V} {u v u' v' : V} {p₁ : G.Walk u v} {p₂ : G.Walk u' v'} (h : p₂.IsSubwalk p₁) : p₂.support ⊆ p₁.support

theorem SimpleGraph.Walk.IsSubwalk.edges_isInfix {V : Type u_1} {G : SimpleGraph V} {u v u' v' : V} {p₁ : G.Walk u v} {p₂ : G.Walk u' v'} (h : p₁.IsSubwalk p₂) : p₁.edges <:+: p₂.edges

@[simp]

theorem SimpleGraph.Walk.IsSubwalk.edges_subset {V : Type u_1} {G : SimpleGraph V} {u v u' v' : V} {p₁ : G.Walk u v} {p₂ : G.Walk u' v'} (h : p₂.IsSubwalk p₁) : p₂.edges ⊆ p₁.edges

theorem SimpleGraph.Walk.IsSubwalk.darts_isInfix {V : Type u_1} {G : SimpleGraph V} {u v u' v' : V} {p₁ : G.Walk u v} {p₂ : G.Walk u' v'} (h : p₁.IsSubwalk p₂) : p₁.darts <:+: p₂.darts

@[simp]

theorem SimpleGraph.Walk.IsSubwalk.darts_subset {V : Type u_1} {G : SimpleGraph V} {u v u' v' : V} {p₁ : G.Walk u v} {p₂ : G.Walk u' v'} (h : p₂.IsSubwalk p₁) : p₂.darts ⊆ p₁.darts

theorem SimpleGraph.Walk.IsSubwalk.map {V : Type u_1} {G G' : SimpleGraph V} {u v u' v' : V} {p₁ : G.Walk u v} {p₂ : G.Walk u' v'} (h : p₂.IsSubwalk p₁) (f : G →g G') : (Walk.map f p₂).IsSubwalk (Walk.map f p₁)

theorem SimpleGraph.Walk.IsSubwalk.copy {V : Type u_1} {G : SimpleGraph V} {u v u' v' x y x' y' : V} {p : G.Walk x y} {q : G.Walk u v} (h : p.IsSubwalk q) (hx : x = x') (hy : y = y') (hu : u = u') (hv : v = v') : (p.copy hx hy).IsSubwalk (q.copy hu hv)

theorem SimpleGraph.Walk.IsSubwalk.dropLast {V : Type u_1} {G : SimpleGraph V} {u v u' v' : V} {p : G.Walk u v} {q : G.Walk u' v'} (hpq : p.IsSubwalk q) : p.dropLast.IsSubwalk q

theorem SimpleGraph.Walk.IsSubwalk.tail {V : Type u_1} {G : SimpleGraph V} {u v u' v' : V} {p : G.Walk u v} {q : G.Walk u' v'} (hpq : p.IsSubwalk q) : p.tail.IsSubwalk q

theorem SimpleGraph.Walk.take_isSubwalk_take {V : Type u_1} {G : SimpleGraph V} {u v : V} {n k : ℕ} (p : G.Walk u v) (h : n ≤ k) : (p.take n).IsSubwalk (p.take k)

theorem SimpleGraph.Walk.drop_isSubwalk_drop {V : Type u_1} {G : SimpleGraph V} {u v : V} {n k : ℕ} (p : G.Walk u v) (h : n ≤ k) : (p.drop k).IsSubwalk (p.drop n)