Metamath Proof Explorer


Definition df-clwlks

Description: Define the set of all closed walks (in an undirected graph).

According to definition 4 in Huneke p. 2: "A walk of length n on (a graph) G is an ordered sequence v0 , v1 , ... v(n) of vertices such that v(i) and v(i+1) are neighbors (i.e are connected by an edge). We say the walk is closed if v(n) = v0".

According to the definition of a walk as two mappings f from { 0 , ... , ( n - 1 ) } and p from { 0 , ... , n }, where f enumerates the (indices of the) edges, and p enumerates the vertices, a closed walk is represented by the following sequence: p(0) e(f(0)) p(1) e(f(1)) ... p(n-1) e(f(n-1)) p(n)=p(0).

Notice that by this definition, a single vertex can be considered as a closed walk of length 0, see also 0clwlk . (Contributed by Alexander van der Vekens, 12-Mar-2018) (Revised by AV, 16-Feb-2021)

Ref Expression
Assertion df-clwlks ClWalks=gVfp|fWalksgpp0=pf

Detailed syntax breakdown

Step Hyp Ref Expression
0 cclwlks classClWalks
1 vg setvarg
2 cvv classV
3 vf setvarf
4 vp setvarp
5 3 cv setvarf
6 cwlks classWalks
7 1 cv setvarg
8 7 6 cfv classWalksg
9 4 cv setvarp
10 5 9 8 wbr wfffWalksgp
11 cc0 class0
12 11 9 cfv classp0
13 chash class.
14 5 13 cfv classf
15 14 9 cfv classpf
16 12 15 wceq wffp0=pf
17 10 16 wa wfffWalksgpp0=pf
18 17 3 4 copab classfp|fWalksgpp0=pf
19 1 2 18 cmpt classgVfp|fWalksgpp0=pf
20 0 19 wceq wffClWalks=gVfp|fWalksgpp0=pf