Trail, Path, and Cycle

In a simple graph,

• A trail is a walk whose edges each appear no more than once.

• A circuit is a nonempty trail whose first and last vertices are the same.

• A path is a trail whose vertices appear no more than once.

• A cycle is a nonempty trail whose first and last vertices are the same and whose vertices except for the first appear no more than once.

Warning: graph theorists mean something different by "path" than do homotopy theorists. A "walk" in graph theory is a "path" in homotopy theory. Another warning: some graph theorists use "path" and "simple path" for "walk" and "path."

Some definitions and theorems have inspiration from multigraph counterparts in [Cho94].

Main definitions

• SimpleGraph.Walk.IsTrail, SimpleGraph.Walk.IsPath, and SimpleGraph.Walk.IsCycle.

• SimpleGraph.Path

• SimpleGraph.Path.map for the induced map on paths, given an (injective) graph homomorphism.

Tags

trails, paths, circuits, cycles

Trails, paths, circuits, cycles

structure SimpleGraph.Walk.IsTrail {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : Prop

A trail is a walk with no repeating edges.

• edges_nodup : p.edges.Nodup

theorem SimpleGraph.Walk.isTrail_def {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.IsTrail ↔ p.edges.Nodup

structure SimpleGraph.Walk.IsPath {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) extends p.IsTrail : Prop

A path is a walk with no repeating vertices. Use SimpleGraph.Walk.IsPath.mk' for a simpler constructor.

• edges_nodup : p.edges.Nodup
• support_nodup : p.support.Nodup

structure SimpleGraph.Walk.IsCircuit {V : Type u} {G : SimpleGraph V} {u : V} (p : G.Walk u u) extends p.IsTrail : Prop

A circuit at u : V is a nonempty trail beginning and ending at u.

• edges_nodup : p.edges.Nodup
• ne_nil : p ≠ nil

theorem SimpleGraph.Walk.isCircuit_def {V : Type u} {G : SimpleGraph V} {u : V} (p : G.Walk u u) : p.IsCircuit ↔ p.IsTrail ∧ p ≠ nil

structure SimpleGraph.Walk.IsCycle {V : Type u} {G : SimpleGraph V} {u : V} (p : G.Walk u u) extends p.IsCircuit : Prop

A cycle at u : V is a circuit at u whose only repeating vertex is u (which appears exactly twice).

• edges_nodup : p.edges.Nodup
• ne_nil : p ≠ nil
• support_nodup : p.support.tail.Nodup

@[deprecated SimpleGraph.Walk.IsPath.isTrail (since := "2025-08-26")]

theorem SimpleGraph.Walk.IsPath.toIsTrail {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (self : p.IsPath) : p.IsTrail

Alias of SimpleGraph.Walk.IsPath.isTrail.

@[deprecated SimpleGraph.Walk.IsCircuit.isTrail (since := "2025-08-26")]

theorem SimpleGraph.Walk.IsCircuit.toIsTrail {V : Type u} {G : SimpleGraph V} {u : V} {p : G.Walk u u} (self : p.IsCircuit) : p.IsTrail

Alias of SimpleGraph.Walk.IsCircuit.isTrail.

@[deprecated SimpleGraph.Walk.IsCycle.isCircuit (since := "2025-08-26")]

theorem SimpleGraph.Walk.IsCycle.toIsCircuit {V : Type u} {G : SimpleGraph V} {u : V} {p : G.Walk u u} (self : p.IsCycle) : p.IsCircuit

Alias of SimpleGraph.Walk.IsCycle.isCircuit.

@[simp]

theorem SimpleGraph.Walk.isTrail_copy {V : Type u} {G : SimpleGraph V} {u v u' v' : V} (p : G.Walk u v) (hu : u = u') (hv : v = v') : (p.copy hu hv).IsTrail ↔ p.IsTrail

theorem SimpleGraph.Walk.IsPath.mk' {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (h : p.support.Nodup) : p.IsPath

theorem SimpleGraph.Walk.isPath_def {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.IsPath ↔ p.support.Nodup

theorem SimpleGraph.Walk.isPath_iff_injective_get_support {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.IsPath ↔ Function.Injective fun (x : Fin p.support.length) => p.support.get x

@[simp]

theorem SimpleGraph.Walk.isPath_copy {V : Type u} {G : SimpleGraph V} {u v u' v' : V} (p : G.Walk u v) (hu : u = u') (hv : v = v') : (p.copy hu hv).IsPath ↔ p.IsPath

@[simp]

theorem SimpleGraph.Walk.isCircuit_copy {V : Type u} {G : SimpleGraph V} {u u' : V} (p : G.Walk u u) (hu : u = u') : (p.copy hu hu).IsCircuit ↔ p.IsCircuit

theorem SimpleGraph.Walk.IsCircuit.not_nil {V : Type u} {G : SimpleGraph V} {v : V} {p : G.Walk v v} (hp : p.IsCircuit) : ¬p.Nil

theorem SimpleGraph.Walk.isCycle_def {V : Type u} {G : SimpleGraph V} {u : V} (p : G.Walk u u) : p.IsCycle ↔ p.IsTrail ∧ p ≠ nil ∧ p.support.tail.Nodup

@[simp]

theorem SimpleGraph.Walk.isCycle_copy {V : Type u} {G : SimpleGraph V} {u u' : V} (p : G.Walk u u) (hu : u = u') : (p.copy hu hu).IsCycle ↔ p.IsCycle

theorem SimpleGraph.Walk.IsCycle.not_nil {V : Type u} {G : SimpleGraph V} {v : V} {p : G.Walk v v} (hp : p.IsCycle) : ¬p.Nil

@[simp]

theorem SimpleGraph.Walk.IsTrail.nil {V : Type u} {G : SimpleGraph V} {u : V} : Walk.nil.IsTrail

theorem SimpleGraph.Walk.IsTrail.of_cons {V : Type u} {G : SimpleGraph V} {u v w : V} {h : G.Adj u v} {p : G.Walk v w} : (cons h p).IsTrail → p.IsTrail

@[simp]

theorem SimpleGraph.Walk.isTrail_cons {V : Type u} {G : SimpleGraph V} {u v w : V} (h : G.Adj u v) (p : G.Walk v w) : (cons h p).IsTrail ↔ p.IsTrail ∧ s(u, v) ∉ p.edges

@[deprecated SimpleGraph.Walk.isTrail_cons (since := "2025-11-03")]

theorem SimpleGraph.Walk.cons_isTrail_iff {V : Type u} {G : SimpleGraph V} {u v w : V} (h : G.Adj u v) (p : G.Walk v w) : (cons h p).IsTrail ↔ p.IsTrail ∧ s(u, v) ∉ p.edges

Alias of SimpleGraph.Walk.isTrail_cons.

theorem SimpleGraph.Walk.IsTrail.cons {V : Type u} {G : SimpleGraph V} {u u' v : V} {w : G.Walk u' v} (hw : w.IsTrail) (hu : G.Adj u u') (hu' : s(u, u') ∉ w.edges) : (cons hu w).IsTrail

theorem SimpleGraph.Walk.IsTrail.reverse {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (h : p.IsTrail) : p.reverse.IsTrail

@[simp]

theorem SimpleGraph.Walk.reverse_isTrail_iff {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.reverse.IsTrail ↔ p.IsTrail

theorem SimpleGraph.Walk.IsTrail.of_append_left {V : Type u} {G : SimpleGraph V} {u v w : V} {p : G.Walk u v} {q : G.Walk v w} (h : (p.append q).IsTrail) : p.IsTrail

theorem SimpleGraph.Walk.IsTrail.of_append_right {V : Type u} {G : SimpleGraph V} {u v w : V} {p : G.Walk u v} {q : G.Walk v w} (h : (p.append q).IsTrail) : q.IsTrail

theorem SimpleGraph.Walk.IsTrail.count_edges_le_one {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v : V} {p : G.Walk u v} (h : p.IsTrail) (e : Sym2 V) : List.count e p.edges ≤ 1

theorem SimpleGraph.Walk.IsTrail.count_edges_eq_one {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v : V} {p : G.Walk u v} (h : p.IsTrail) {e : Sym2 V} (he : e ∈ p.edges) : List.count e p.edges = 1

theorem SimpleGraph.Walk.IsTrail.length_le_card_edgeFinset {V : Type u} {G : SimpleGraph V} [Fintype ↑G.edgeSet] {u v : V} {w : G.Walk u v} (h : w.IsTrail) : w.length ≤ G.edgeFinset.card

theorem SimpleGraph.Walk.IsPath.nil {V : Type u} {G : SimpleGraph V} {u : V} : Walk.nil.IsPath

theorem SimpleGraph.Walk.IsPath.of_cons {V : Type u} {G : SimpleGraph V} {u v w : V} {h : G.Adj u v} {p : G.Walk v w} : (cons h p).IsPath → p.IsPath

@[simp]

theorem SimpleGraph.Walk.cons_isPath_iff {V : Type u} {G : SimpleGraph V} {u v w : V} (h : G.Adj u v) (p : G.Walk v w) : (cons h p).IsPath ↔ p.IsPath ∧ u ∉ p.support

theorem SimpleGraph.Walk.IsPath.cons {V : Type u} {G : SimpleGraph V} {u v w : V} {p : G.Walk v w} (hp : p.IsPath) (hu : u ∉ p.support) {h : G.Adj u v} : (cons h p).IsPath

@[simp]

theorem SimpleGraph.Walk.isPath_iff_eq_nil {V : Type u} {G : SimpleGraph V} {u : V} (p : G.Walk u u) : p.IsPath ↔ p = nil

theorem SimpleGraph.Walk.IsPath.reverse {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (h : p.IsPath) : p.reverse.IsPath

@[simp]

theorem SimpleGraph.Walk.isPath_reverse_iff {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.reverse.IsPath ↔ p.IsPath

theorem SimpleGraph.Walk.IsPath.of_append_left {V : Type u} {G : SimpleGraph V} {u v w : V} {p : G.Walk u v} {q : G.Walk v w} : (p.append q).IsPath → p.IsPath

theorem SimpleGraph.Walk.IsPath.of_append_right {V : Type u} {G : SimpleGraph V} {u v w : V} {p : G.Walk u v} {q : G.Walk v w} (h : (p.append q).IsPath) : q.IsPath

theorem SimpleGraph.Walk.isTrail_of_isSubwalk {V : Type u} {G : SimpleGraph V} {v w v' w' : V} {p₁ : G.Walk v w} {p₂ : G.Walk v' w'} (h : p₁.IsSubwalk p₂) (h₂ : p₂.IsTrail) : p₁.IsTrail

theorem SimpleGraph.Walk.isPath_of_isSubwalk {V : Type u} {G : SimpleGraph V} {v w v' w' : V} {p₁ : G.Walk v w} {p₂ : G.Walk v' w'} (h : p₁.IsSubwalk p₂) (h₂ : p₂.IsPath) : p₁.IsPath

theorem SimpleGraph.Walk.IsPath.of_adj {V : Type u} {G : SimpleGraph V} {u v : V} (h : G.Adj u v) : h.toWalk.IsPath

theorem SimpleGraph.Walk.concat_isPath_iff {V : Type u} {G : SimpleGraph V} {u v w : V} {p : G.Walk u v} (h : G.Adj v w) : (p.concat h).IsPath ↔ p.IsPath ∧ w ∉ p.support

theorem SimpleGraph.Walk.IsPath.concat {V : Type u} {G : SimpleGraph V} {u v w : V} {p : G.Walk u v} (hp : p.IsPath) (hw : w ∉ p.support) (h : G.Adj v w) : (p.concat h).IsPath

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

theorem SimpleGraph.Walk.IsPath.disjoint_support_of_append {V : Type u} {G : SimpleGraph V} {u v w : V} {p : G.Walk u v} {q : G.Walk v w} (hpq : (p.append q).IsPath) (hq : ¬q.Nil) : p.support.Disjoint q.tail.support

theorem SimpleGraph.Walk.IsPath.ne_of_mem_support_of_append {V : Type u} {G : SimpleGraph V} {u v w : V} {p : G.Walk u v} {q : G.Walk v w} (hpq : (p.append q).IsPath) {x y : V} (hyv : y ≠ v) (hx : x ∈ p.support) (hy : y ∈ q.support) : x ≠ y

@[simp]

theorem SimpleGraph.Walk.IsCycle.not_of_nil {V : Type u} {G : SimpleGraph V} {u : V} : ¬nil.IsCycle

theorem SimpleGraph.Walk.IsCycle.ne_bot {V : Type u} {G : SimpleGraph V} {u : V} {p : G.Walk u u} : p.IsCycle → G ≠ ⊥

theorem SimpleGraph.Walk.IsCycle.three_le_length {V : Type u} {G : SimpleGraph V} {v : V} {p : G.Walk v v} (hp : p.IsCycle) : 3 ≤ p.length

theorem SimpleGraph.Walk.not_nil_of_isCycle_cons {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} {h : G.Adj v u} (hc : (cons h p).IsCycle) : ¬p.Nil

theorem SimpleGraph.Walk.cons_isCycle_iff {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk v u) (h : G.Adj u v) : (cons h p).IsCycle ↔ p.IsPath ∧ s(u, v) ∉ p.edges

theorem SimpleGraph.Walk.IsCycle.reverse {V : Type u} {G : SimpleGraph V} {u : V} {p : G.Walk u u} (h : p.IsCycle) : p.reverse.IsCycle

@[simp]

theorem SimpleGraph.Walk.isCycle_reverse {V : Type u} {G : SimpleGraph V} {u : V} {p : G.Walk u u} : p.reverse.IsCycle ↔ p.IsCycle

theorem SimpleGraph.Walk.IsCycle.isPath_of_append_right {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} {q : G.Walk v u} (h : ¬p.Nil) (hcyc : (p.append q).IsCycle) : q.IsPath

theorem SimpleGraph.Walk.IsCycle.isPath_of_append_left {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} {q : G.Walk v u} (h : ¬q.Nil) (hcyc : (p.append q).IsCycle) : p.IsPath

theorem SimpleGraph.Walk.IsPath.tail {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (hp : p.IsPath) : p.tail.IsPath

About paths

instance SimpleGraph.Walk.instDecidableIsPathOfDecidableEq {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v : V} (p : G.Walk u v) : Decidable p.IsPath

Equations

• p.instDecidableIsPathOfDecidableEq = ⋯.mpr inferInstance

theorem SimpleGraph.Walk.IsPath.length_lt {V : Type u} {G : SimpleGraph V} [Fintype V] {u v : V} {p : G.Walk u v} (hp : p.IsPath) : p.length < Fintype.card V

theorem SimpleGraph.Walk.IsPath.getVert_injOn {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (hp : p.IsPath) : Set.InjOn p.getVert {i : ℕ | i ≤ p.length}

theorem SimpleGraph.Walk.IsPath.getVert_eq_start_iff {V : Type u} {G : SimpleGraph V} {u w : V} {i : ℕ} {p : G.Walk u w} (hp : p.IsPath) (hi : i ≤ p.length) : p.getVert i = u ↔ i = 0

theorem SimpleGraph.Walk.IsPath.getVert_eq_end_iff {V : Type u} {G : SimpleGraph V} {u w : V} {i : ℕ} {p : G.Walk u w} (hp : p.IsPath) (hi : i ≤ p.length) : p.getVert i = w ↔ i = p.length

theorem SimpleGraph.Walk.IsPath.getVert_injOn_iff {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : Set.InjOn p.getVert {i : ℕ | i ≤ p.length} ↔ p.IsPath

theorem SimpleGraph.Walk.IsPath.eq_snd_of_mem_edges {V : Type u} {G : SimpleGraph V} {u v w : V} {p : G.Walk u v} (hp : p.IsPath) (hnil : ¬p.Nil) (hmem : s(u, w) ∈ p.edges) : w = p.snd

theorem SimpleGraph.Walk.IsPath.eq_penultimate_of_mem_edges {V : Type u} {G : SimpleGraph V} {u v w : V} {p : G.Walk u v} (hp : p.IsPath) (hnil : ¬p.Nil) (hmem : s(v, w) ∈ p.edges) : w = p.penultimate

About cycles

theorem SimpleGraph.Walk.IsCycle.getVert_injOn {V : Type u} {G : SimpleGraph V} {u : V} {p : G.Walk u u} (hpc : p.IsCycle) : Set.InjOn p.getVert {i : ℕ | 1 ≤ i ∧ i ≤ p.length}

theorem SimpleGraph.Walk.IsCycle.getVert_injOn' {V : Type u} {G : SimpleGraph V} {u : V} {p : G.Walk u u} (hpc : p.IsCycle) : Set.InjOn p.getVert {i : ℕ | i ≤ p.length - 1}

theorem SimpleGraph.Walk.IsCycle.snd_ne_penultimate {V : Type u} {G : SimpleGraph V} {u : V} {p : G.Walk u u} (hp : p.IsCycle) : p.snd ≠ p.penultimate

theorem SimpleGraph.Walk.IsCycle.getVert_endpoint_iff {V : Type u} {G : SimpleGraph V} {u : V} {i : ℕ} {p : G.Walk u u} (hpc : p.IsCycle) (hl : i ≤ p.length) : p.getVert i = u ↔ i = 0 ∨ i = p.length

theorem SimpleGraph.Walk.IsCycle.getVert_sub_one_ne_getVert_add_one {V : Type u} {G : SimpleGraph V} {u : V} {i : ℕ} {p : G.Walk u u} (hpc : p.IsCycle) (h : i ≤ p.length) : p.getVert (i - 1) ≠ p.getVert (i + 1)

@[deprecated SimpleGraph.Walk.IsCycle.getVert_sub_one_ne_getVert_add_one (since := "2025-04-27")]

theorem SimpleGraph.Walk.IsCycle.getVert_sub_one_neq_getVert_add_one {V : Type u} {G : SimpleGraph V} {u : V} {i : ℕ} {p : G.Walk u u} (hpc : p.IsCycle) (h : i ≤ p.length) : p.getVert (i - 1) ≠ p.getVert (i + 1)

Alias of SimpleGraph.Walk.IsCycle.getVert_sub_one_ne_getVert_add_one.

Walk decompositions

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

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

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

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

theorem SimpleGraph.Walk.IsTrail.disjoint_edges_takeUntil_dropUntil {V : Type u} {G : SimpleGraph V} {u v : V} [DecidableEq V] {x : V} {w : G.Walk u v} (hw : w.IsTrail) (hx : x ∈ w.support) : (w.takeUntil x hx).edges.Disjoint (w.dropUntil x hx).edges

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

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

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

theorem SimpleGraph.Walk.IsCycle.isPath_takeUntil {V : Type u} {G : SimpleGraph V} {v w : V} [DecidableEq V] {c : G.Walk v v} (hc : c.IsCycle) (h : w ∈ c.support) : (c.takeUntil w h).IsPath

theorem SimpleGraph.Walk.IsCycle.count_support {V : Type u} {G : SimpleGraph V} {v : V} [DecidableEq V] {c : G.Walk v v} (hc : c.IsCycle) : List.count v c.support = 2

theorem SimpleGraph.Walk.IsCycle.count_support_of_mem {V : Type u} {G : SimpleGraph V} {u v : V} [DecidableEq V] {c : G.Walk v v} (hc : c.IsCycle) (hu : u ∈ c.support) (hv : u ≠ v) : List.count u c.support = 1

theorem SimpleGraph.Walk.endpoint_notMem_support_takeUntil {V : Type u} {G : SimpleGraph V} {u v w : V} [DecidableEq V] {p : G.Walk u v} (hp : p.IsPath) (hw : w ∈ p.support) (h : v ≠ w) : v ∉ (p.takeUntil w hw).support

Taking a strict initial segment of a path removes the end vertex from the support.

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

theorem SimpleGraph.Walk.endpoint_not_mem_support_takeUntil {V : Type u} {G : SimpleGraph V} {u v w : V} [DecidableEq V] {p : G.Walk u v} (hp : p.IsPath) (hw : w ∈ p.support) (h : v ≠ w) : v ∉ (p.takeUntil w hw).support

Alias of SimpleGraph.Walk.endpoint_notMem_support_takeUntil.

---

Taking a strict initial segment of a path removes the end vertex from the support.

Type of paths

@[reducible, inline]

abbrev SimpleGraph.Path {V : Type u} (G : SimpleGraph V) (u v : V) : Type u

The type for paths between two vertices.

Equations

• G.Path u v = { p : G.Walk u v // p.IsPath }

@[simp]

theorem SimpleGraph.Path.isPath {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Path u v) : (↑p).IsPath

@[simp]

theorem SimpleGraph.Path.isTrail {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Path u v) : (↑p).IsTrail

def SimpleGraph.Path.nil {V : Type u} {G : SimpleGraph V} {u : V} : G.Path u u

The length-0 path at a vertex.

Equations

• SimpleGraph.Path.nil = ⟨SimpleGraph.Walk.nil, ⋯⟩

@[simp]

theorem SimpleGraph.Path.nil_coe {V : Type u} {G : SimpleGraph V} {u : V} : ↑Path.nil = Walk.nil

def SimpleGraph.Path.singleton {V : Type u} {G : SimpleGraph V} {u v : V} (h : G.Adj u v) : G.Path u v

The length-1 path between a pair of adjacent vertices.

Equations

• SimpleGraph.Path.singleton h = ⟨SimpleGraph.Walk.cons h SimpleGraph.Walk.nil, ⋯⟩

@[simp]

theorem SimpleGraph.Path.singleton_coe {V : Type u} {G : SimpleGraph V} {u v : V} (h : G.Adj u v) : ↑(singleton h) = Walk.cons h Walk.nil

theorem SimpleGraph.Path.mk'_mem_edges_singleton {V : Type u} {G : SimpleGraph V} {u v : V} (h : G.Adj u v) : s(u, v) ∈ (↑(singleton h)).edges

def SimpleGraph.Path.reverse {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Path u v) : G.Path v u

The reverse of a path is another path. See also SimpleGraph.Walk.reverse.

Equations

• p.reverse = ⟨(↑p).reverse, ⋯⟩

@[simp]

theorem SimpleGraph.Path.reverse_coe {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Path u v) : ↑p.reverse = (↑p).reverse

theorem SimpleGraph.Path.count_support_eq_one {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v w : V} {p : G.Path u v} (hw : w ∈ (↑p).support) : List.count w (↑p).support = 1

theorem SimpleGraph.Path.count_edges_eq_one {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v : V} {p : G.Path u v} (e : Sym2 V) (hw : e ∈ (↑p).edges) : List.count e (↑p).edges = 1

@[simp]

theorem SimpleGraph.Path.nodup_support {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Path u v) : (↑p).support.Nodup

theorem SimpleGraph.Path.loop_eq {V : Type u} {G : SimpleGraph V} {v : V} (p : G.Path v v) : p = Path.nil

theorem SimpleGraph.Path.notMem_edges_of_loop {V : Type u} {G : SimpleGraph V} {v : V} {e : Sym2 V} {p : G.Path v v} : e ∉ (↑p).edges

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

theorem SimpleGraph.Path.not_mem_edges_of_loop {V : Type u} {G : SimpleGraph V} {v : V} {e : Sym2 V} {p : G.Path v v} : e ∉ (↑p).edges

Alias of SimpleGraph.Path.notMem_edges_of_loop.

theorem SimpleGraph.Path.cons_isCycle {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Path v u) (h : G.Adj u v) (he : s(u, v) ∉ (↑p).edges) : (Walk.cons h ↑p).IsCycle

Walks to paths

def SimpleGraph.Walk.bypass {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v : V} : G.Walk u v → G.Walk u v

Given a walk, produces a walk from it by bypassing subwalks between repeated vertices. The result is a path, as shown in SimpleGraph.Walk.bypass_isPath. This is packaged up in SimpleGraph.Walk.toPath.

Equations

• SimpleGraph.Walk.nil.bypass = SimpleGraph.Walk.nil
• (SimpleGraph.Walk.cons ha p).bypass = if hs : u ∈ p.bypass.support then p.bypass.dropUntil u hs else SimpleGraph.Walk.cons ha p.bypass

@[simp]

theorem SimpleGraph.Walk.bypass_copy {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u u' v v' : V} (p : G.Walk u v) (hu : u = u') (hv : v = v') : (p.copy hu hv).bypass = p.bypass.copy hu hv

theorem SimpleGraph.Walk.bypass_isPath {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v : V} (p : G.Walk u v) : p.bypass.IsPath

theorem SimpleGraph.Walk.length_bypass_le {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v : V} (p : G.Walk u v) : p.bypass.length ≤ p.length

theorem SimpleGraph.Walk.bypass_eq_self_of_length_le {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v : V} (p : G.Walk u v) (h : p.length ≤ p.bypass.length) : p.bypass = p

def SimpleGraph.Walk.toPath {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v : V} (p : G.Walk u v) : G.Path u v

Given a walk, produces a path with the same endpoints using SimpleGraph.Walk.bypass.

Equations

• p.toPath = ⟨p.bypass, ⋯⟩

theorem SimpleGraph.Walk.support_bypass_subset {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v : V} (p : G.Walk u v) : p.bypass.support ⊆ p.support

theorem SimpleGraph.Walk.support_toPath_subset {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v : V} (p : G.Walk u v) : (↑p.toPath).support ⊆ p.support

theorem SimpleGraph.Walk.darts_bypass_subset {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v : V} (p : G.Walk u v) : p.bypass.darts ⊆ p.darts

theorem SimpleGraph.Walk.edges_bypass_subset {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v : V} (p : G.Walk u v) : p.bypass.edges ⊆ p.edges

theorem SimpleGraph.Walk.darts_toPath_subset {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v : V} (p : G.Walk u v) : (↑p.toPath).darts ⊆ p.darts

theorem SimpleGraph.Walk.edges_toPath_subset {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v : V} (p : G.Walk u v) : (↑p.toPath).edges ⊆ p.edges

def SimpleGraph.Walk.cycleBypass {V : Type u} {G : SimpleGraph V} [DecidableEq V] {v : V} : G.Walk v v → G.Walk v v

Bypass repeated vertices like Walk.bypass, except the starting vertex.

This is intended to be used for closed walks, for which Walk.bypass unhelpfully returns the empty walk.

Equations

• SimpleGraph.Walk.nil.cycleBypass = SimpleGraph.Walk.nil
• (SimpleGraph.Walk.cons hvv' w).cycleBypass = SimpleGraph.Walk.cons hvv' w.bypass

@[simp]

theorem SimpleGraph.Walk.cycleBypass_nil {V : Type u} {G : SimpleGraph V} [DecidableEq V] {v : V} : nil.cycleBypass = nil

theorem SimpleGraph.Walk.edges_cycleBypass_subset {V : Type u} {G : SimpleGraph V} [DecidableEq V] {v : V} {w : G.Walk v v} : w.cycleBypass.edges ⊆ w.edges

theorem SimpleGraph.Walk.IsTrail.isCycle_cycleBypass {V : Type u} {G : SimpleGraph V} [DecidableEq V] {v : V} {w : G.Walk v v} : w ≠ Walk.nil → w.IsTrail → w.cycleBypass.IsCycle

Mapping paths

theorem SimpleGraph.Walk.map_isPath_of_injective {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G →g G'} {u v : V} {p : G.Walk u v} (hinj : Function.Injective ⇑f) (hp : p.IsPath) : (Walk.map f p).IsPath

theorem SimpleGraph.Walk.IsPath.of_map {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {u v : V} {p : G.Walk u v} {f : G →g G'} (hp : (Walk.map f p).IsPath) : p.IsPath

theorem SimpleGraph.Walk.map_isPath_iff_of_injective {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G →g G'} {u v : V} {p : G.Walk u v} (hinj : Function.Injective ⇑f) : (Walk.map f p).IsPath ↔ p.IsPath

theorem SimpleGraph.Walk.map_isTrail_iff_of_injective {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G →g G'} {u v : V} {p : G.Walk u v} (hinj : Function.Injective ⇑f) : (Walk.map f p).IsTrail ↔ p.IsTrail

theorem SimpleGraph.Walk.map_isTrail_of_injective {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G →g G'} {u v : V} {p : G.Walk u v} (hinj : Function.Injective ⇑f) : p.IsTrail → (Walk.map f p).IsTrail

Alias of the reverse direction of SimpleGraph.Walk.map_isTrail_iff_of_injective.

theorem SimpleGraph.Walk.map_isCycle_iff_of_injective {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G →g G'} {u : V} {p : G.Walk u u} (hinj : Function.Injective ⇑f) : (Walk.map f p).IsCycle ↔ p.IsCycle

theorem SimpleGraph.Walk.IsCycle.map {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G →g G'} {u : V} {p : G.Walk u u} (hinj : Function.Injective ⇑f) : p.IsCycle → (Walk.map f p).IsCycle

Alias of the reverse direction of SimpleGraph.Walk.map_isCycle_iff_of_injective.

@[simp]

theorem SimpleGraph.Walk.mapLe_isTrail {V : Type u} {G G' : SimpleGraph V} (h : G ≤ G') {u v : V} {p : G.Walk u v} : (mapLe h p).IsTrail ↔ p.IsTrail

theorem SimpleGraph.Walk.IsTrail.mapLe {V : Type u} {G G' : SimpleGraph V} (h : G ≤ G') {u v : V} {p : G.Walk u v} : p.IsTrail → (Walk.mapLe h p).IsTrail

Alias of the reverse direction of SimpleGraph.Walk.mapLe_isTrail.

theorem SimpleGraph.Walk.IsTrail.of_mapLe {V : Type u} {G G' : SimpleGraph V} (h : G ≤ G') {u v : V} {p : G.Walk u v} : (Walk.mapLe h p).IsTrail → p.IsTrail

Alias of the forward direction of SimpleGraph.Walk.mapLe_isTrail.

@[simp]

theorem SimpleGraph.Walk.mapLe_isPath {V : Type u} {G G' : SimpleGraph V} (h : G ≤ G') {u v : V} {p : G.Walk u v} : (mapLe h p).IsPath ↔ p.IsPath

theorem SimpleGraph.Walk.IsPath.of_mapLe {V : Type u} {G G' : SimpleGraph V} (h : G ≤ G') {u v : V} {p : G.Walk u v} : (Walk.mapLe h p).IsPath → p.IsPath

Alias of the forward direction of SimpleGraph.Walk.mapLe_isPath.

theorem SimpleGraph.Walk.IsPath.mapLe {V : Type u} {G G' : SimpleGraph V} (h : G ≤ G') {u v : V} {p : G.Walk u v} : p.IsPath → (Walk.mapLe h p).IsPath

Alias of the reverse direction of SimpleGraph.Walk.mapLe_isPath.

@[simp]

theorem SimpleGraph.Walk.mapLe_isCycle {V : Type u} {G G' : SimpleGraph V} (h : G ≤ G') {u : V} {p : G.Walk u u} : (mapLe h p).IsCycle ↔ p.IsCycle

theorem SimpleGraph.Walk.IsCycle.of_mapLe {V : Type u} {G G' : SimpleGraph V} (h : G ≤ G') {u : V} {p : G.Walk u u} : (Walk.mapLe h p).IsCycle → p.IsCycle

Alias of the forward direction of SimpleGraph.Walk.mapLe_isCycle.

theorem SimpleGraph.Walk.IsCycle.mapLe {V : Type u} {G G' : SimpleGraph V} (h : G ≤ G') {u : V} {p : G.Walk u u} : p.IsCycle → (Walk.mapLe h p).IsCycle

Alias of the reverse direction of SimpleGraph.Walk.mapLe_isCycle.

def SimpleGraph.Path.map {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') (hinj : Function.Injective ⇑f) {u v : V} (p : G.Path u v) : G'.Path (f u) (f v)

Given an injective graph homomorphism, map paths to paths.

Equations

• SimpleGraph.Path.map f hinj p = ⟨SimpleGraph.Walk.map f ↑p, ⋯⟩

@[simp]

theorem SimpleGraph.Path.map_coe {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') (hinj : Function.Injective ⇑f) {u v : V} (p : G.Path u v) : ↑(Path.map f hinj p) = Walk.map f ↑p

theorem SimpleGraph.Path.map_injective {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G →g G'} (hinj : Function.Injective ⇑f) (u v : V) : Function.Injective (Path.map f hinj)

def SimpleGraph.Path.mapEmbedding {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G ↪g G') {u v : V} (p : G.Path u v) : G'.Path (f u) (f v)

Given a graph embedding, map paths to paths.

Equations

• SimpleGraph.Path.mapEmbedding f p = SimpleGraph.Path.map f.toHom ⋯ p

@[simp]

theorem SimpleGraph.Path.mapEmbedding_coe {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G ↪g G') {u v : V} (p : G.Path u v) : ↑(Path.mapEmbedding f p) = Walk.map f.toHom ↑p

theorem SimpleGraph.Path.mapEmbedding_injective {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G ↪g G') (u v : V) : Function.Injective (Path.mapEmbedding f)

Transferring between graphs

theorem SimpleGraph.Walk.IsPath.transfer {V : Type u} {G : SimpleGraph V} {u v : V} {H : SimpleGraph V} {p : G.Walk u v} (hp : ∀ e ∈ p.edges, e ∈ H.edgeSet) (pp : p.IsPath) : (p.transfer H hp).IsPath

theorem SimpleGraph.Walk.IsCycle.transfer {V : Type u} {G : SimpleGraph V} {u : V} {H : SimpleGraph V} {q : G.Walk u u} (qc : q.IsCycle) (hq : ∀ e ∈ q.edges, e ∈ H.edgeSet) : (q.transfer H hq).IsCycle

Deleting edges

theorem SimpleGraph.Walk.IsPath.toDeleteEdges {V : Type u} (G : SimpleGraph V) {v w : V} (s : Set (Sym2 V)) {p : G.Walk v w} (h : p.IsPath) (hp : ∀ e ∈ p.edges, e ∉ s) : (toDeleteEdges s p hp).IsPath

theorem SimpleGraph.Walk.IsCycle.toDeleteEdges {V : Type u} (G : SimpleGraph V) {v : V} (s : Set (Sym2 V)) {p : G.Walk v v} (h : p.IsCycle) (hp : ∀ e ∈ p.edges, e ∉ s) : (toDeleteEdges s p hp).IsCycle

@[simp]

theorem SimpleGraph.Walk.toDeleteEdges_copy {V : Type u} (G : SimpleGraph V) {v u u' v' : V} (s : Set (Sym2 V)) (p : G.Walk u v) (hu : u = u') (hv : v = v') (h : ∀ e ∈ (p.copy hu hv).edges, e ∉ s) : toDeleteEdges s (p.copy hu hv) h = (toDeleteEdges s p ⋯).copy hu hv