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.

Equations

• One or more equations did not get rendered due to their size.
• SimpleGraph.Walk.nil.takeUntil x x_1 = ⋯.mpr SimpleGraph.Walk.nil

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.

Equations

• One or more equations did not get rendered due to their size.
• SimpleGraph.Walk.nil.dropUntil x x_1 = ⋯.mpr SimpleGraph.Walk.nil

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

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.

Equations

• c.rotate h = (c.dropUntil u h).append (c.takeUntil u h)

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