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

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.

Equations

• p.IsSubwalk q = ∃ (ru : G.Walk u₂ u₁) (rv : G.Walk v₁ v₂), q = (ru.append p).append rv

@[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.nil_isSubwalk {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.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_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_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₁)