Decomposing walks

Main definitions

• takeUntil: The path obtained by taking edges of an existing path until a given vertex.
• dropUntil: The path obtained by dropping edges of an existing path until a given vertex.
• rotate: Rotate a loop walk such that it is centered at the given vertex.

Walk decompositions

def SimpleGraph.Walk.takeUntil {V : Type u} {G : SimpleGraph V} [DecidableEq V] {v w : V} (p : G.Walk v w) (u : V) : u ∈ p.support → G.Walk v u

Given a vertex in the support of a path, give the path up until (and including) that vertex.

@[simp]

theorem SimpleGraph.Walk.takeUntil_nil {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {h : u ∈ nil.support} : nil.takeUntil u h = nil

theorem SimpleGraph.Walk.takeUntil_cons {V : Type u} {G : SimpleGraph V} {v w u : V} [DecidableEq V] {v' : V} {p : G.Walk v' v} (hwp : w ∈ p.support) (h : u ≠ w) (hadj : G.Adj u v') : (cons hadj p).takeUntil w ⋯ = cons hadj (p.takeUntil w hwp)

@[simp]

theorem SimpleGraph.Walk.takeUntil_first {V : Type u} {G : SimpleGraph V} {v u : V} [DecidableEq V] (p : G.Walk u v) : p.takeUntil u ⋯ = nil

@[simp]

theorem SimpleGraph.Walk.nil_takeUntil {V : Type u} {G : SimpleGraph V} {v w u : V} [DecidableEq V] (p : G.Walk u v) (hwp : w ∈ p.support) : (p.takeUntil w hwp).Nil ↔ u = w

def SimpleGraph.Walk.dropUntil {V : Type u} {G : SimpleGraph V} [DecidableEq V] {v w : V} (p : G.Walk v w) (u : V) : u ∈ p.support → G.Walk u w

Given a vertex in the support of a path, give the path from (and including) that vertex to the end. In other words, drop vertices from the front of a path until (and not including) that vertex.

@[simp]

theorem SimpleGraph.Walk.take_spec {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v w : V} (p : G.Walk v w) (h : u ∈ p.support) : (p.takeUntil u h).append (p.dropUntil u h) = p

The takeUntil and dropUntil functions split a walk into two pieces. The lemma SimpleGraph.Walk.count_support_takeUntil_eq_one specifies where this split occurs.

theorem SimpleGraph.Walk.mem_support_iff_exists_append {V : Type u} {G : SimpleGraph V} {u v w : V} {p : G.Walk u v} : w ∈ p.support ↔ ∃ (q : G.Walk u w) (r : G.Walk w v), p = q.append r

@[simp]

theorem SimpleGraph.Walk.count_support_takeUntil_eq_one {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v w : V} (p : G.Walk v w) (h : u ∈ p.support) : List.count u (p.takeUntil u h).support = 1

theorem SimpleGraph.Walk.count_edges_takeUntil_le_one {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v w : V} (p : G.Walk v w) (h : u ∈ p.support) (x : V) : List.count s(u, x) (p.takeUntil u h).edges ≤ 1

@[simp]

theorem SimpleGraph.Walk.takeUntil_copy {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v w v' w' : V} (p : G.Walk v w) (hv : v = v') (hw : w = w') (h : u ∈ (p.copy hv hw).support) : (p.copy hv hw).takeUntil u h = (p.takeUntil u ⋯).copy hv ⋯

@[simp]

theorem SimpleGraph.Walk.dropUntil_copy {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v w v' w' : V} (p : G.Walk v w) (hv : v = v') (hw : w = w') (h : u ∈ (p.copy hv hw).support) : (p.copy hv hw).dropUntil u h = (p.dropUntil u ⋯).copy ⋯ hw

theorem SimpleGraph.Walk.support_takeUntil_subset {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v w : V} (p : G.Walk v w) (h : u ∈ p.support) : (p.takeUntil u h).support ⊆ p.support

theorem SimpleGraph.Walk.support_dropUntil_subset {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v w : V} (p : G.Walk v w) (h : u ∈ p.support) : (p.dropUntil u h).support ⊆ p.support

theorem SimpleGraph.Walk.darts_takeUntil_subset {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v w : V} (p : G.Walk v w) (h : u ∈ p.support) : (p.takeUntil u h).darts ⊆ p.darts

theorem SimpleGraph.Walk.darts_dropUntil_subset {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v w : V} (p : G.Walk v w) (h : u ∈ p.support) : (p.dropUntil u h).darts ⊆ p.darts

theorem SimpleGraph.Walk.edges_takeUntil_subset {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v w : V} (p : G.Walk v w) (h : u ∈ p.support) : (p.takeUntil u h).edges ⊆ p.edges

theorem SimpleGraph.Walk.edges_dropUntil_subset {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v w : V} (p : G.Walk v w) (h : u ∈ p.support) : (p.dropUntil u h).edges ⊆ p.edges

theorem SimpleGraph.Walk.length_takeUntil_le {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v w : V} (p : G.Walk v w) (h : u ∈ p.support) : (p.takeUntil u h).length ≤ p.length

theorem SimpleGraph.Walk.length_dropUntil_le {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v w : V} (p : G.Walk v w) (h : u ∈ p.support) : (p.dropUntil u h).length ≤ p.length

@[irreducible]

theorem SimpleGraph.Walk.getVert_takeUntil {V : Type u} {G : SimpleGraph V} {w : V} [DecidableEq V] {u v : V} {n : ℕ} {p : G.Walk u v} (hw : w ∈ p.support) (hn : n ≤ (p.takeUntil w hw).length) : (p.takeUntil w hw).getVert n = p.getVert n

theorem SimpleGraph.Walk.snd_takeUntil {V : Type u} {G : SimpleGraph V} {v w u : V} [DecidableEq V] (hsu : w ≠ u) (p : G.Walk u v) (h : w ∈ p.support) : (p.takeUntil w h).snd = p.snd

theorem SimpleGraph.Walk.length_takeUntil_lt {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v w : V} {p : G.Walk v w} (h : u ∈ p.support) (huw : u ≠ w) : (p.takeUntil u h).length < p.length

theorem SimpleGraph.Walk.takeUntil_takeUntil {V : Type u} {G : SimpleGraph V} {v u : V} [DecidableEq V] {w x : V} (p : G.Walk u v) (hw : w ∈ p.support) (hx : x ∈ (p.takeUntil w hw).support) : (p.takeUntil w hw).takeUntil x hx = p.takeUntil x ⋯

theorem SimpleGraph.Walk.notMem_support_takeUntil_support_takeUntil_subset {V : Type u} {G : SimpleGraph V} {v u : V} [DecidableEq V] {p : G.Walk u v} {w x : V} (h : x ≠ w) (hw : w ∈ p.support) (hx : x ∈ (p.takeUntil w hw).support) : w ∉ (p.takeUntil x ⋯).support

@[deprecated SimpleGraph.Walk.notMem_support_takeUntil_support_takeUntil_subset (since := "2025-05-23")]

theorem SimpleGraph.Walk.not_mem_support_takeUntil_support_takeUntil_subset {V : Type u} {G : SimpleGraph V} {v u : V} [DecidableEq V] {p : G.Walk u v} {w x : V} (h : x ≠ w) (hw : w ∈ p.support) (hx : x ∈ (p.takeUntil w hw).support) : w ∉ (p.takeUntil x ⋯).support

Alias of SimpleGraph.Walk.notMem_support_takeUntil_support_takeUntil_subset.

def SimpleGraph.Walk.rotate {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v : V} (c : G.Walk v v) (h : u ∈ c.support) : G.Walk u u

Rotate a loop walk such that it is centered at the given vertex.

@[simp]

theorem SimpleGraph.Walk.support_rotate {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v : V} (c : G.Walk v v) (h : u ∈ c.support) : (c.rotate h).support.tail ~r c.support.tail

theorem SimpleGraph.Walk.rotate_darts {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v : V} (c : G.Walk v v) (h : u ∈ c.support) : (c.rotate h).darts ~r c.darts

theorem SimpleGraph.Walk.rotate_edges {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v : V} (c : G.Walk v v) (h : u ∈ c.support) : (c.rotate h).edges ~r c.edges

@[irreducible]

theorem SimpleGraph.Walk.mem_support_iff_exists_getVert {V : Type u} {G : SimpleGraph V} {u v w : V} {p : G.Walk v w} : u ∈ p.support ↔ ∃ (n : ℕ), p.getVert n = u ∧ n ≤ p.length

Given a walk w and a node in the support, there exists a natural n, such that given node is the n-th node (zero-indexed) in the walk. In addition, n is at most the length of the path. Due to the definition of getVert it would otherwise be legal to return a larger n for the last node.