Counting walks of a given length

Main definitions

• walkLengthTwoEquivCommonNeighbors: bijective correspondence between walks of length two from u to v and common neighbours of u and v. Note that u and v may be the same.
• finsetWalkLength: the Finset of length-n walks from u to v. This is used to give {p : G.walk u v | p.length = n} a Fintype instance, and it can also be useful as a recursive description of this set when V is finite.

TODO: should this be extended further?

theorem SimpleGraph.Walk.setOfPred_length_eq_zero {V : Type u} (G : SimpleGraph V) (u : V) : {p : G.Walk u u | p.length = 0} = {nil}

@[deprecated SimpleGraph.Walk.setOfPred_length_eq_zero (since := "2026-07-09")]

theorem SimpleGraph.Walk.setOf_length_eq_zero {V : Type u} (G : SimpleGraph V) (u : V) : {p : G.Walk u u | p.length = 0} = {nil}

Alias of SimpleGraph.Walk.setOfPred_length_eq_zero.

@[deprecated SimpleGraph.Walk.setOfPred_length_eq_zero (since := "2026-05-12")]

theorem SimpleGraph.set_walk_self_length_zero_eq {V : Type u} (G : SimpleGraph V) (u : V) : {p : G.Walk u u | p.length = 0} = {Walk.nil}

Alias of SimpleGraph.Walk.setOfPred_length_eq_zero.

theorem SimpleGraph.Walk.setOfPred_length_eq_zero_of_ne {V : Type u} (G : SimpleGraph V) {u v : V} (h : u ≠ v) : {p : G.Walk u v | p.length = 0} = ∅

@[deprecated SimpleGraph.Walk.setOfPred_length_eq_zero_of_ne (since := "2026-07-09")]

theorem SimpleGraph.Walk.setOf_length_eq_zero_of_ne {V : Type u} (G : SimpleGraph V) {u v : V} (h : u ≠ v) : {p : G.Walk u v | p.length = 0} = ∅

Alias of SimpleGraph.Walk.setOfPred_length_eq_zero_of_ne.

@[deprecated SimpleGraph.Walk.setOfPred_length_eq_zero_of_ne (since := "2026-05-12")]

theorem SimpleGraph.set_walk_length_zero_eq_of_ne {V : Type u} (G : SimpleGraph V) {u v : V} (h : u ≠ v) : {p : G.Walk u v | p.length = 0} = ∅

Alias of SimpleGraph.Walk.setOfPred_length_eq_zero_of_ne.

theorem SimpleGraph.Walk.setOfPred_length_eq_add_one {V : Type u} (G : SimpleGraph V) (u v : V) (n : ℕ) : {p : G.Walk u v | p.length = n + 1} = ⋃ (w : V), ⋃ (h : G.Adj u w), cons h '' {p' : G.Walk w v | p'.length = n}

@[deprecated SimpleGraph.Walk.setOfPred_length_eq_add_one (since := "2026-07-09")]

theorem SimpleGraph.Walk.setOf_length_eq_add_one {V : Type u} (G : SimpleGraph V) (u v : V) (n : ℕ) : {p : G.Walk u v | p.length = n + 1} = ⋃ (w : V), ⋃ (h : G.Adj u w), cons h '' {p' : G.Walk w v | p'.length = n}

Alias of SimpleGraph.Walk.setOfPred_length_eq_add_one.

@[deprecated SimpleGraph.Walk.setOfPred_length_eq_add_one (since := "2026-05-12")]

theorem SimpleGraph.set_walk_length_succ_eq {V : Type u} (G : SimpleGraph V) (u v : V) (n : ℕ) : {p : G.Walk u v | p.length = n + 1} = ⋃ (w : V), ⋃ (h : G.Adj u w), Walk.cons h '' {p' : G.Walk w v | p'.length = n}

Alias of SimpleGraph.Walk.setOfPred_length_eq_add_one.

def SimpleGraph.walkLengthTwoEquivCommonNeighbors {V : Type u} (G : SimpleGraph V) (u v : V) : { p : G.Walk u v // p.length = 2 } ≃ ↑(G.commonNeighbors u v)

Walks of length two from u to v correspond bijectively to common neighbours of u and v. Note that u and v may be the same.

@[simp]

theorem SimpleGraph.walkLengthTwoEquivCommonNeighbors_symm_apply_coe {V : Type u} (G : SimpleGraph V) (u v : V) (w : ↑(G.commonNeighbors u v)) : ↑((G.walkLengthTwoEquivCommonNeighbors u v).symm w) = (Adj.toWalk ⋯).concat ⋯

@[simp]

theorem SimpleGraph.walkLengthTwoEquivCommonNeighbors_apply_coe {V : Type u} (G : SimpleGraph V) (u v : V) (p : { p : G.Walk u v // p.length = 2 }) : ↑((G.walkLengthTwoEquivCommonNeighbors u v) p) = (↑p).snd

def SimpleGraph.finsetWalkLength {V : Type u} (G : SimpleGraph V) [DecidableEq V] [G.LocallyFinite] (n : ℕ) (u v : V) : Finset (G.Walk u v)

The Finset of length-n walks from u to v. This is used to give {p : G.walk u v | p.length = n} a Fintype instance, and it can also be useful as a recursive description of this set when V is finite.

See SimpleGraph.coe_finsetWalkLength_eq for the relationship between this Finset and the set of length-n walks.

theorem SimpleGraph.coe_finsetWalkLength_eq {V : Type u} (G : SimpleGraph V) [DecidableEq V] [G.LocallyFinite] (n : ℕ) (u v : V) : ↑(G.finsetWalkLength n u v) = {p : G.Walk u v | p.length = n}

theorem SimpleGraph.mem_finsetWalkLength_iff {V : Type u} {G : SimpleGraph V} [DecidableEq V] [G.LocallyFinite] {n : ℕ} {u v : V} {p : G.Walk u v} : p ∈ G.finsetWalkLength n u v ↔ p.length = n

def SimpleGraph.finsetWalkLengthLT {V : Type u} (G : SimpleGraph V) [DecidableEq V] [G.LocallyFinite] (n : ℕ) (u v : V) : Finset (G.Walk u v)

The Finset of walks from u to v with length less than n. See finsetWalkLength for context. In particular, we use this definition for SimpleGraph.Path.instFintype.

theorem SimpleGraph.coe_finsetWalkLengthLT_eq {V : Type u} (G : SimpleGraph V) [DecidableEq V] [G.LocallyFinite] (n : ℕ) (u v : V) : ↑(G.finsetWalkLengthLT n u v) = {p : G.Walk u v | p.length < n}

theorem SimpleGraph.mem_finsetWalkLengthLT_iff {V : Type u} {G : SimpleGraph V} [DecidableEq V] [G.LocallyFinite] {n : ℕ} {u v : V} {p : G.Walk u v} : p ∈ G.finsetWalkLengthLT n u v ↔ p.length < n

@[instance_reducible]

instance SimpleGraph.fintypeSetWalkLength {V : Type u} (G : SimpleGraph V) [DecidableEq V] [G.LocallyFinite] (u v : V) (n : ℕ) : Fintype ↑{p : G.Walk u v | p.length = n}

@[instance_reducible]

instance SimpleGraph.fintypeSubtypeWalkLength {V : Type u} (G : SimpleGraph V) [DecidableEq V] [G.LocallyFinite] (u v : V) (n : ℕ) : Fintype { p : G.Walk u v // p.length = n }

theorem SimpleGraph.set_walk_length_toFinset_eq {V : Type u} (G : SimpleGraph V) [DecidableEq V] [G.LocallyFinite] (n : ℕ) (u v : V) : {p : G.Walk u v | p.length = n}.toFinset = G.finsetWalkLength n u v

theorem SimpleGraph.card_set_walk_length_eq {V : Type u} (G : SimpleGraph V) [DecidableEq V] [G.LocallyFinite] (u v : V) (n : ℕ) : Fintype.card ↑{p : G.Walk u v | p.length = n} = (G.finsetWalkLength n u v).card

See SimpleGraph.adjMatrix_pow_apply_eq_card_walk for the cardinality in terms of the nth power of the adjacency matrix.

@[instance_reducible]

instance SimpleGraph.fintypeSetWalkLengthLT {V : Type u} (G : SimpleGraph V) [DecidableEq V] [G.LocallyFinite] (u v : V) (n : ℕ) : Fintype ↑{p : G.Walk u v | p.length < n}

@[instance_reducible]

instance SimpleGraph.fintypeSubtypeWalkLengthLT {V : Type u} (G : SimpleGraph V) [DecidableEq V] [G.LocallyFinite] (u v : V) (n : ℕ) : Fintype { p : G.Walk u v // p.length < n }

@[instance_reducible]

instance SimpleGraph.fintypeSetPathLength {V : Type u} (G : SimpleGraph V) [DecidableEq V] [G.LocallyFinite] (u v : V) (n : ℕ) : Fintype ↑{p : G.Walk u v | p.IsPath ∧ p.length = n}

@[instance_reducible]

instance SimpleGraph.fintypeSubtypePathLength {V : Type u} (G : SimpleGraph V) [DecidableEq V] [G.LocallyFinite] (u v : V) (n : ℕ) : Fintype { p : G.Walk u v // p.IsPath ∧ p.length = n }

@[instance_reducible]

instance SimpleGraph.fintypeSetPathLengthLT {V : Type u} (G : SimpleGraph V) [DecidableEq V] [G.LocallyFinite] (u v : V) (n : ℕ) : Fintype ↑{p : G.Walk u v | p.IsPath ∧ p.length < n}

@[instance_reducible]

instance SimpleGraph.fintypeSubtypePathLengthLT {V : Type u} (G : SimpleGraph V) [DecidableEq V] [G.LocallyFinite] (u v : V) (n : ℕ) : Fintype { p : G.Walk u v // p.IsPath ∧ p.length < n }

@[instance_reducible]

instance SimpleGraph.Path.instFintype {V : Type u} (G : SimpleGraph V) [DecidableEq V] [Fintype V] [DecidableRel G.Adj] {u v : V} : Fintype (G.Path u v)