English
For each n, the set of length-n walks from u to v is a finite set (a Finset) when the vertex set is finite.
Русский
Для каждого n множество ходов длины n от u до v является конечным множеством (Finset), если множество вершин конечное.
LaTeX
$$def finsetWalkLength (n : ℕ) (u v : V) : Finset (G.Walk u v)$$
Lean4
/-- 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. -/
def finsetWalkLength (n : ℕ) (u v : V) : Finset (G.Walk u v) :=
match n with
| 0 =>
if h : u = v then by
subst u
exact { Walk.nil }
else ∅
| n + 1 =>
Finset.univ.biUnion fun (w : G.neighborSet u) =>
(finsetWalkLength n w v).map ⟨fun p => Walk.cons w.property p, fun _ _ => by simp⟩
