Walks in multigraphs

This file defines edge-labelled walks in Mathlib's Graph. Unlike walks in a simple graph, a walk records the identity of each edge it traverses. Thus parallel edges give distinct walks, while a loop has one length-one traversal. The basic API includes vertex and edge lists, concatenation, reversal, paths, cycles, internally disjoint walks, and the induced reachability relation.

The interface follows Mathlib's SimpleGraph.Walk, adapted so that walks retain actual multigraph edge identities. The path-composition lemma Graph.Walk.IsPath.isCycle_append is adapted from Mathlib's theorem of the same name for simple-graph walks.

inductive Graph.Walk {α : Type u} {β : Type v} (G : Graph α β) : α → α → Type (max u v)

An edge-labelled walk in a multigraph. Each step records an edge together with its incidence; a zero-length walk may be based at any ambient point.

• nil {α : Type u} {β : Type v} {G : Graph α β} {x : α} : G.Walk x x
• cons {α : Type u} {β : Type v} {G : Graph α β} {x y z : α} (e : β) (h : G.IsLink e x y) (p : G.Walk y z) : G.Walk x z

@[reducible, match_pattern, inline]

abbrev Graph.Walk.nil' {α : Type u} {β : Type v} {G : Graph α β} (x : α) : G.Walk x x

Pattern for a length-zero walk with its vertex explicit.

@[reducible, match_pattern, inline]

abbrev Graph.Walk.cons' {α : Type u} {β : Type v} {G : Graph α β} (x y z : α) (e : β) (h : G.IsLink e x y) (p : G.Walk y z) : G.Walk x z

Pattern for a nonempty walk with all three vertices explicit.

@[instance_reducible]

instance Graph.Walk.instInhabited {α : Type u} {β : Type v} {G : Graph α β} (x : α) : Inhabited (G.Walk x x)

def Graph.Walk.copy {α : Type u} {β : Type v} {G : Graph α β} {x y x' y' : α} (p : G.Walk x y) (hx : x = x') (hy : y = y') : G.Walk x' y'

Change the endpoints of a walk along equalities.

@[simp]

theorem Graph.Walk.copy_rfl_rfl {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (p : G.Walk x y) : p.copy ⋯ ⋯ = p

@[simp]

theorem Graph.Walk.copy_copy {α : Type u} {β : Type v} {G : Graph α β} {x y x' y' x'' y'' : α} (p : G.Walk x y) (hx : x = x') (hy : y = y') (hx' : x' = x'') (hy' : y' = y'') : (p.copy hx hy).copy hx' hy' = p.copy ⋯ ⋯

@[simp]

theorem Graph.Walk.copy_nil {α : Type u} {β : Type v} {G : Graph α β} {x x' : α} (hx : x = x') : nil.copy hx hx = nil

@[simp]

theorem Graph.Walk.copy_cons {α : Type u} {β : Type v} {G : Graph α β} {x y z x' z' : α} (e : β) (h : G.IsLink e x y) (p : G.Walk y z) (hx : x = x') (hz : z = z') : (cons e h p).copy hx hz = cons e ⋯ (p.copy ⋯ hz)

def Graph.IsLink.toWalk {α : Type u} {β : Type v} {G : Graph α β} {x y : α} {e : β} (h : G.IsLink e x y) : G.Walk x y

The one-edge walk associated to an edge linking two vertices.

theorem Graph.IsLink.toWalk_eq_cons {α : Type u} {β : Type v} {G : Graph α β} {x y : α} {e : β} (h : G.IsLink e x y) : h.toWalk = Walk.cons e h Walk.nil

A one-edge walk is the corresponding cons followed by the empty walk.

def Graph.Walk.length {α : Type u} {β : Type v} {G : Graph α β} {x y : α} : G.Walk x y → ℕ

The number of edge traversals in a walk.

def Graph.Walk.support {α : Type u} {β : Type v} {G : Graph α β} {x y : α} : G.Walk x y → List α

The vertices visited by a walk, in order and including both endpoints.

def Graph.Walk.edges {α : Type u} {β : Type v} {G : Graph α β} {x y : α} : G.Walk x y → List β

The edges traversed by a walk, in order and with repetitions.

theorem Graph.Walk.edges_subset_edgeSet {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (p : G.Walk x y) ⦃e : β⦄ : e ∈ p.edges → e ∈ G.edgeSet

Every edge traversed by a walk is an actual edge of the ambient graph.

def Graph.Walk.edgesAttach {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (p : G.Walk x y) : List ↑G.edgeSet

The edges traversed by a walk, as actual edges.

@[simp]

theorem Graph.Walk.edgesAttach_nil {α : Type u} {β : Type v} {G : Graph α β} {x : α} : nil.edgesAttach = []

@[simp]

theorem Graph.Walk.edgesAttach_cons {α : Type u} {β : Type v} {G : Graph α β} {x y z : α} (e : β) (h : G.IsLink e x y) (p : G.Walk y z) : (cons e h p).edgesAttach = ⟨e, ⋯⟩ :: p.edgesAttach

@[simp]

theorem Graph.Walk.edgesAttach_unattach {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (p : G.Walk x y) : p.edgesAttach.unattach = p.edges

Forgetting actual-edge membership from edgesAttach gives the edge list.

@[simp]

theorem Graph.Walk.length_nil {α : Type u} {β : Type v} {G : Graph α β} {x : α} : nil.length = 0

@[simp]

theorem Graph.Walk.length_cons {α : Type u} {β : Type v} {G : Graph α β} {x y z : α} (e : β) (h : G.IsLink e x y) (p : G.Walk y z) : (cons e h p).length = p.length + 1

@[simp]

theorem Graph.Walk.support_nil {α : Type u} {β : Type v} {G : Graph α β} {x : α} : nil.support = [x]

@[simp]

theorem Graph.Walk.support_cons {α : Type u} {β : Type v} {G : Graph α β} {x y z : α} (e : β) (h : G.IsLink e x y) (p : G.Walk y z) : (cons e h p).support = x :: p.support

@[simp]

theorem Graph.Walk.edges_nil {α : Type u} {β : Type v} {G : Graph α β} {x : α} : nil.edges = []

@[simp]

theorem Graph.Walk.edges_cons {α : Type u} {β : Type v} {G : Graph α β} {x y z : α} (e : β) (h : G.IsLink e x y) (p : G.Walk y z) : (cons e h p).edges = e :: p.edges

@[simp]

theorem Graph.Walk.length_copy {α : Type u} {β : Type v} {G : Graph α β} {x y x' y' : α} (p : G.Walk x y) (hx : x = x') (hy : y = y') : (p.copy hx hy).length = p.length

@[simp]

theorem Graph.Walk.support_copy {α : Type u} {β : Type v} {G : Graph α β} {x y x' y' : α} (p : G.Walk x y) (hx : x = x') (hy : y = y') : (p.copy hx hy).support = p.support

@[simp]

theorem Graph.Walk.edges_copy {α : Type u} {β : Type v} {G : Graph α β} {x y x' y' : α} (p : G.Walk x y) (hx : x = x') (hy : y = y') : (p.copy hx hy).edges = p.edges

@[simp]

theorem Graph.IsLink.length_toWalk {α : Type u} {β : Type v} {G : Graph α β} {x y : α} {e : β} (h : G.IsLink e x y) : h.toWalk.length = 1

@[simp]

theorem Graph.IsLink.support_toWalk {α : Type u} {β : Type v} {G : Graph α β} {x y : α} {e : β} (h : G.IsLink e x y) : h.toWalk.support = [x, y]

@[simp]

theorem Graph.IsLink.edges_toWalk {α : Type u} {β : Type v} {G : Graph α β} {x y : α} {e : β} (h : G.IsLink e x y) : h.toWalk.edges = [e]

@[simp]

theorem Graph.Walk.support_ne_nil {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (p : G.Walk x y) : p.support ≠ []

@[simp]

theorem Graph.Walk.head_support {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (p : G.Walk x y) : p.support.head ⋯ = x

@[simp]

theorem Graph.Walk.getLast_support {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (p : G.Walk x y) : p.support.getLast ⋯ = y

@[simp]

theorem Graph.Walk.cons_tail_support {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (p : G.Walk x y) : x :: p.support.tail = p.support

theorem Graph.Walk.mem_support_iff {α : Type u} {β : Type v} {G : Graph α β} {x y a : α} (p : G.Walk x y) : a ∈ p.support ↔ a = x ∨ a ∈ p.support.tail

@[simp]

theorem Graph.Walk.start_mem_support {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (p : G.Walk x y) : x ∈ p.support

@[simp]

theorem Graph.Walk.end_mem_support {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (p : G.Walk x y) : y ∈ p.support

@[simp]

theorem Graph.Walk.length_edges {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (p : G.Walk x y) : p.edges.length = p.length

@[simp]

theorem Graph.Walk.length_support {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (p : G.Walk x y) : p.support.length = p.length + 1

theorem Graph.Walk.eq_of_length_eq_zero {α : Type u} {β : Type v} {G : Graph α β} {x y : α} {p : G.Walk x y} (hp : p.length = 0) : x = y

inductive Graph.Walk.Nil {α : Type u} {β : Type v} {G : Graph α β} {x y : α} : G.Walk x y → Prop

A walk is nil when it consists of no steps.

• nil {α : Type u} {β : Type v} {G : Graph α β} {x : α} : Walk.nil.Nil

@[simp]

theorem Graph.Walk.nil_nil {α : Type u} {β : Type v} {G : Graph α β} {x : α} : nil.Nil

@[simp]

theorem Graph.Walk.not_nil_cons {α : Type u} {β : Type v} {G : Graph α β} {x y z : α} {e : β} {h : G.IsLink e x y} {p : G.Walk y z} : ¬(cons e h p).Nil

@[simp]

theorem Graph.Walk.length_eq_zero_iff {α : Type u} {β : Type v} {G : Graph α β} {x y : α} {p : G.Walk x y} : p.length = 0 ↔ p.Nil

theorem Graph.Walk.ext_edges {α : Type u} {β : Type v} {G : Graph α β} {x y : α} {p q : G.Walk x y} (h : p.edges = q.edges) : p = q

An edge-labelled walk is determined by its starting vertex and its edge sequence.

theorem Graph.Walk.ext_edges_iff {α : Type u} {β : Type v} {G : Graph α β} {x y : α} {p q : G.Walk x y} : p = q ↔ p.edges = q.edges

@[simp]

theorem Graph.Walk.edges_eq_nil {α : Type u} {β : Type v} {G : Graph α β} {x y : α} {p : G.Walk x y} : p.edges = [] ↔ p.Nil

theorem Graph.Walk.Nil.eq {α : Type u} {β : Type v} {G : Graph α β} {x y : α} {p : G.Walk x y} : p.Nil → x = y

theorem Graph.Walk.nil_iff_support_eq {α : Type u} {β : Type v} {G : Graph α β} {x y : α} {p : G.Walk x y} : p.Nil ↔ p.support = [x]

@[simp]

theorem Graph.Walk.eq_nil_iff_nil {α : Type u} {β : Type v} {G : Graph α β} {x : α} {p : G.Walk x x} : p = nil ↔ p.Nil

A walk with definitionally equal endpoints is nil exactly when it equals nil.

theorem Graph.Walk.Nil.eq_nil {α : Type u} {β : Type v} {G : Graph α β} {x : α} {p : G.Walk x x} : p.Nil → p = Walk.nil

Alias of the reverse direction of Graph.Walk.eq_nil_iff_nil.

---

A walk with definitionally equal endpoints is nil exactly when it equals nil.

theorem Graph.Walk.support_subset_vertexSet {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (p : G.Walk x y) (hx : x ∈ G.vertexSet) (a : α) : a ∈ p.support → a ∈ G.vertexSet

Every vertex on a walk starting at an actual vertex is an actual vertex of the ambient graph.

theorem Graph.Walk.support_subset_vertexSet_of_pos {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (p : G.Walk x y) (hp : 0 < p.length) (a : α) : a ∈ p.support → a ∈ G.vertexSet

Every vertex on a positive-length walk is an actual vertex of the ambient graph.

theorem Graph.Walk.mem_support_of_isLink_of_mem_edges {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (p : G.Walk x y) {a b : α} {e : β} (h : G.IsLink e a b) (he : e ∈ p.edges) : a ∈ p.support

An endpoint of an edge traversed by a walk occurs in the walk's support.

theorem Graph.Walk.end_mem_support_of_edges_subset {α : Type u} {β : Type v} {G : Graph α β} {x y a b : α} (r : G.Walk a b) (q : G.Walk x y) (h : r.edges ⊆ q.edges) (ha : a ∈ q.support) : b ∈ q.support

If a walk uses only edges of another walk and starts in its support, it ends there too.

theorem Graph.Walk.edges_nodup_of_support_nodup {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (p : G.Walk x y) (hp : p.support.Nodup) : p.edges.Nodup

A walk with no repeated vertices also has no repeated edge identities.

def Graph.Walk.append {α : Type u} {β : Type v} {G : Graph α β} {x y z : α} : G.Walk x y → G.Walk y z → G.Walk x z

Concatenation of two walks whose adjacent endpoints agree.

@[simp]

theorem Graph.Walk.nil_append {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (p : G.Walk x y) : nil.append p = p

@[simp]

theorem Graph.Walk.cons_append {α : Type u} {β : Type v} {G : Graph α β} {x y z w : α} (e : β) (h : G.IsLink e x y) (p : G.Walk y z) (q : G.Walk z w) : (cons e h p).append q = cons e h (p.append q)

@[simp]

theorem Graph.Walk.append_nil {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (p : G.Walk x y) : p.append nil = p

theorem Graph.Walk.append_assoc {α : Type u} {β : Type v} {G : Graph α β} {x y z w : α} (p : G.Walk x y) (q : G.Walk y z) (r : G.Walk z w) : p.append (q.append r) = (p.append q).append r

@[simp]

theorem Graph.Walk.append_copy_copy {α : Type u} {β : Type v} {G : Graph α β} {x y z x' y' z' : α} (p : G.Walk x y) (q : G.Walk y z) (hx : x = x') (hy : y = y') (hz : z = z') : (p.copy hx hy).append (q.copy hy hz) = (p.append q).copy hx hz

@[simp]

theorem Graph.Walk.length_append {α : Type u} {β : Type v} {G : Graph α β} {x y z : α} (p : G.Walk x y) (q : G.Walk y z) : (p.append q).length = p.length + q.length

@[simp]

theorem Graph.Walk.edges_append {α : Type u} {β : Type v} {G : Graph α β} {x y z : α} (p : G.Walk x y) (q : G.Walk y z) : (p.append q).edges = p.edges ++ q.edges

@[simp]

theorem Graph.Walk.support_append {α : Type u} {β : Type v} {G : Graph α β} {x y z : α} (p : G.Walk x y) (q : G.Walk y z) : (p.append q).support = p.support ++ q.support.tail

theorem Graph.Walk.support_append_eq_support_dropLast_append {α : Type u} {β : Type v} {G : Graph α β} {x y z : α} (p : G.Walk x y) (q : G.Walk y z) : (p.append q).support = p.support.dropLast ++ q.support

def Graph.Walk.reverseAux {α : Type u} {β : Type v} {G : Graph α β} {x y z : α} : G.Walk x y → G.Walk x z → G.Walk y z

Auxiliary tail-recursive operation used to reverse a walk.

def Graph.Walk.reverse {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (p : G.Walk x y) : G.Walk y x

A walk traversed backwards, retaining the same edge identities.

@[simp]

theorem Graph.Walk.reverse_nil {α : Type u} {β : Type v} {G : Graph α β} {x : α} : nil.reverse = nil

@[simp]

theorem Graph.IsLink.reverse_toWalk {α : Type u} {β : Type v} {G : Graph α β} {x y : α} {e : β} (h : G.IsLink e x y) : h.toWalk.reverse = ⋯.toWalk

@[simp]

theorem Graph.Walk.reverseAux_append {α : Type u} {β : Type v} {G : Graph α β} {x y z w : α} (p : G.Walk x y) (q : G.Walk x z) (r : G.Walk z w) : (p.reverseAux q).append r = p.reverseAux (q.append r)

@[simp]

theorem Graph.Walk.append_reverseAux {α : Type u} {β : Type v} {G : Graph α β} {x y z w : α} (p : G.Walk x y) (q : G.Walk y z) (r : G.Walk x w) : (p.append q).reverseAux r = q.reverseAux (p.reverseAux r)

theorem Graph.Walk.reverseAux_eq_reverse_append {α : Type u} {β : Type v} {G : Graph α β} {x y z : α} (p : G.Walk x y) (q : G.Walk x z) : p.reverseAux q = p.reverse.append q

@[simp]

theorem Graph.Walk.reverse_cons {α : Type u} {β : Type v} {G : Graph α β} {x y z : α} (e : β) (h : G.IsLink e x y) (p : G.Walk y z) : (cons e h p).reverse = p.reverse.append ⋯.toWalk

@[simp]

theorem Graph.Walk.reverse_copy {α : Type u} {β : Type v} {G : Graph α β} {x y x' y' : α} (p : G.Walk x y) (hx : x = x') (hy : y = y') : (p.copy hx hy).reverse = p.reverse.copy hy hx

@[simp]

theorem Graph.Walk.reverse_append {α : Type u} {β : Type v} {G : Graph α β} {x y z : α} (p : G.Walk x y) (q : G.Walk y z) : (p.append q).reverse = q.reverse.append p.reverse

@[simp]

theorem Graph.Walk.reverse_reverse {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (p : G.Walk x y) : p.reverse.reverse = p

@[simp]

theorem Graph.Walk.length_reverse {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (p : G.Walk x y) : p.reverse.length = p.length

@[simp]

theorem Graph.Walk.edges_reverse {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (p : G.Walk x y) : p.reverse.edges = p.edges.reverse

@[simp]

theorem Graph.Walk.support_reverse {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (p : G.Walk x y) : p.reverse.support = p.support.reverse

theorem Graph.Walk.tail_support_perm_dropLast_support {α : Type u} {β : Type v} {G : Graph α β} {x : α} (p : G.Walk x x) : p.support.tail.Perm p.support.dropLast

def Graph.Walk.IsTrail {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (p : G.Walk x y) : Prop

A trail is a walk that traverses no edge identity more than once.

def Graph.Walk.IsPath {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (p : G.Walk x y) : Prop

A path is a walk that visits no vertex more than once.

def Graph.Walk.IsCycle {α : Type u} {β : Type v} {G : Graph α β} {x : α} (p : G.Walk x x) : Prop

A cycle is a nonempty closed trail whose only repeated vertex is its base vertex.

theorem Graph.Walk.isTrail_def {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (p : G.Walk x y) : p.IsTrail ↔ p.edges.Nodup

theorem Graph.Walk.isPath_def {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (p : G.Walk x y) : p.IsPath ↔ p.support.Nodup

theorem Graph.Walk.isCycle_def {α : Type u} {β : Type v} {G : Graph α β} {x : α} (p : G.Walk x x) : p.IsCycle ↔ p ≠ nil ∧ p.edges.Nodup ∧ p.support.tail.Nodup

@[simp]

theorem Graph.Walk.isTrail_copy {α : Type u} {β : Type v} {G : Graph α β} {x y x' y' : α} (p : G.Walk x y) (hx : x = x') (hy : y = y') : (p.copy hx hy).IsTrail ↔ p.IsTrail

@[simp]

theorem Graph.Walk.isPath_copy {α : Type u} {β : Type v} {G : Graph α β} {x y x' y' : α} (p : G.Walk x y) (hx : x = x') (hy : y = y') : (p.copy hx hy).IsPath ↔ p.IsPath

@[simp]

theorem Graph.Walk.isCycle_copy {α : Type u} {β : Type v} {G : Graph α β} {x x' : α} (p : G.Walk x x) (hx : x = x') : (p.copy hx hx).IsCycle ↔ p.IsCycle

@[simp]

theorem Graph.Walk.isTrail_nil {α : Type u} {β : Type v} {G : Graph α β} {x : α} : nil.IsTrail

@[simp]

theorem Graph.Walk.isTrail_cons {α : Type u} {β : Type v} {G : Graph α β} {x y z : α} (e : β) (h : G.IsLink e x y) (p : G.Walk y z) : (cons e h p).IsTrail ↔ p.IsTrail ∧ e ∉ p.edges

@[simp]

theorem Graph.Walk.isPath_cons {α : Type u} {β : Type v} {G : Graph α β} {x y z : α} (e : β) (h : G.IsLink e x y) (p : G.Walk y z) : (cons e h p).IsPath ↔ p.IsPath ∧ x ∉ p.support

@[simp]

theorem Graph.Walk.isPath_iff_nil {α : Type u} {β : Type v} {G : Graph α β} {x : α} {p : G.Walk x x} : p.IsPath ↔ p.Nil

A walk with equal endpoints is a path exactly when it consists of no steps.

@[simp]

theorem Graph.Walk.cons_isCycle_iff {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (e : β) (h : G.IsLink e x y) (p : G.Walk y x) : (cons e h p).IsCycle ↔ p.IsPath ∧ e ∉ p.edges

theorem Graph.Walk.IsPath.isTrail {α : Type u} {β : Type v} {G : Graph α β} {x y : α} {p : G.Walk x y} (hp : p.IsPath) : p.IsTrail

Every path is a trail.

theorem Graph.Walk.IsPath.support_nodup {α : Type u} {β : Type v} {G : Graph α β} {x y : α} {p : G.Walk x y} (hp : p.IsPath) : p.support.Nodup

@[simp]

theorem Graph.IsLink.isPath_toWalk_iff {α : Type u} {β : Type v} {G : Graph α β} {x y : α} {e : β} (h : G.IsLink e x y) : h.toWalk.IsPath ↔ x ≠ y

@[simp]

theorem Graph.Walk.isTrail_reverse {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (p : G.Walk x y) : p.reverse.IsTrail ↔ p.IsTrail

@[simp]

theorem Graph.Walk.isPath_reverse {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (p : G.Walk x y) : p.reverse.IsPath ↔ p.IsPath

@[simp]

theorem Graph.Walk.not_isCycle_nil {α : Type u} {β : Type v} {G : Graph α β} {x : α} : ¬nil.IsCycle

theorem Graph.Walk.IsCycle.isTrail {α : Type u} {β : Type v} {G : Graph α β} {x : α} {p : G.Walk x x} (hp : p.IsCycle) : p.IsTrail

theorem Graph.Walk.IsCycle.ne_nil {α : Type u} {β : Type v} {G : Graph α β} {x : α} {p : G.Walk x x} (hp : p.IsCycle) : p ≠ nil

theorem Graph.Walk.IsCycle.not_nil {α : Type u} {β : Type v} {G : Graph α β} {x : α} {p : G.Walk x x} (hp : p.IsCycle) : ¬p.Nil

theorem Graph.Walk.IsCycle.support_tail_nodup {α : Type u} {β : Type v} {G : Graph α β} {x : α} {p : G.Walk x x} (hp : p.IsCycle) : p.support.tail.Nodup

@[simp]

theorem Graph.IsLink.isCycle_toWalk {α : Type u} {β : Type v} {G : Graph α β} {x : α} {e : β} (h : G.IsLink e x x) : h.toWalk.IsCycle

@[simp]

theorem Graph.Walk.isCycle_reverse {α : Type u} {β : Type v} {G : Graph α β} {x : α} (p : G.Walk x x) : p.reverse.IsCycle ↔ p.IsCycle

theorem Graph.Walk.IsPath.isCycle_append {α : Type u} {β : Type v} {G : Graph α β} {x y : α} {p : G.Walk x y} {q : G.Walk y x} (hp : p.IsPath) (hq : q.IsPath) (hv : p.support.tail.Disjoint q.support.tail) (he : p.edges.Disjoint q.edges) (hne : 0 < p.length ∨ 0 < q.length) : (p.append q).IsCycle

Two paths with opposite endpoints form a cycle when their interiors and edge identities are disjoint and at least one path is nonempty.

def Graph.Walk.InternallyDisjoint {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (p q : G.Walk x y) : Prop

Two walks from x to y are internally disjoint when they share no vertex other than x and y.

theorem Graph.Walk.internallyDisjoint_def {α : Type u} {β : Type v} {G : Graph α β} {x y : α} {p q : G.Walk x y} : p.InternallyDisjoint q ↔ ∀ v ∈ p.support, v ∈ q.support → v = x ∨ v = y

theorem Graph.Walk.InternallyDisjoint.symm {α : Type u} {β : Type v} {G : Graph α β} {x y : α} {p q : G.Walk x y} (h : p.InternallyDisjoint q) : q.InternallyDisjoint p

theorem Graph.Walk.internallyDisjoint_comm {α : Type u} {β : Type v} {G : Graph α β} {x y : α} {p q : G.Walk x y} : p.InternallyDisjoint q ↔ q.InternallyDisjoint p

def Graph.Reachable {α : Type u} {β : Type v} (G : Graph α β) (x y : α) : Prop

Two ambient points are reachable when the first is an actual vertex and an edge-labelled walk joins them. The endpoint is then automatically an actual vertex as well.

theorem Graph.reachable_def {α : Type u} {β : Type v} {G : Graph α β} {x y : α} : G.Reachable x y ↔ x ∈ G.vertexSet ∧ Nonempty (G.Walk x y)

theorem Graph.Walk.end_mem_vertexSet {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (p : G.Walk x y) (hx : x ∈ G.vertexSet) : y ∈ G.vertexSet

theorem Graph.Walk.reachable {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (p : G.Walk x y) (hx : x ∈ G.vertexSet) : G.Reachable x y

A walk starting at an actual vertex witnesses reachability.

theorem Graph.IsLink.reachable {α : Type u} {β : Type v} {G : Graph α β} {x y : α} {e : β} (h : G.IsLink e x y) : G.Reachable x y

The endpoints of a link are reachable.

theorem Graph.Reachable.left_mem {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (h : G.Reachable x y) : x ∈ G.vertexSet

theorem Graph.Reachable.right_mem {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (h : G.Reachable x y) : y ∈ G.vertexSet

theorem Graph.Reachable.elim {α : Type u} {β : Type v} {G : Graph α β} {x y : α} {p : Prop} (h : G.Reachable x y) (hp : ∀ (a : G.Walk x y), p) : p

theorem Graph.Reachable.refl {α : Type u} {β : Type v} {G : Graph α β} {x : α} (hx : x ∈ G.vertexSet) : G.Reachable x x

Every actual vertex is reachable from itself.

theorem Graph.Reachable.symm {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (h : G.Reachable x y) : G.Reachable y x

Multigraph reachability is symmetric.

theorem Graph.Reachable.trans {α : Type u} {β : Type v} {G : Graph α β} {x y z : α} (hxy : G.Reachable x y) (hyz : G.Reachable y z) : G.Reachable x z

Multigraph reachability is transitive.

@[simp]

theorem Graph.reachable_self_iff {α : Type u} {β : Type v} {G : Graph α β} {x : α} : G.Reachable x x ↔ x ∈ G.vertexSet

A point is reachable from itself exactly when it is an actual vertex.

theorem Graph.reachable_is_equivalence {α : Type u} {β : Type v} (G : Graph α β) : Equivalence fun (x y : ↑G.vertexSet) => G.Reachable ↑x ↑y

Reachability is an equivalence relation on the actual vertices of a graph.

theorem Graph.IsClosedSubgraph.mem_vertexSet_of_reachable {α : Type u} {β : Type v} {G H : Graph α β} (hHG : H.IsClosedSubgraph G) {x y : α} (hx : x ∈ H.vertexSet) (hxy : G.Reachable x y) : y ∈ H.vertexSet

Membership in a closed subgraph propagates along reachability.