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 = ( g e. _V |-> { <. f , p >. | ( f ( Walks ` g ) p /\ ( p ` 0 ) = ( p ` ( # ` f ) ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cclwlks	|- ClWalks
1		vg	|- g
2		cvv	|- _V
3		vf	|- f
4		vp	|- p
5	3	cv	|- f
6		cwlks	|- Walks
7	1	cv	|- g
8	7 6	cfv	|- ( Walks ` g )
9	4	cv	|- p
10	5 9 8	wbr	|- f ( Walks ` g ) p
11		cc0	|- 0
12	11 9	cfv	|- ( p ` 0 )
13		chash	|- #
14	5 13	cfv	|- ( # ` f )
15	14 9	cfv	|- ( p ` ( # ` f ) )
16	12 15	wceq	|- ( p ` 0 ) = ( p ` ( # ` f ) )
17	10 16	wa	|- ( f ( Walks ` g ) p /\ ( p ` 0 ) = ( p ` ( # ` f ) ) )
18	17 3 4	copab	|- { <. f , p >. | ( f ( Walks ` g ) p /\ ( p ` 0 ) = ( p ` ( # ` f ) ) ) }
19	1 2 18	cmpt	|- ( g e. _V |-> { <. f , p >. | ( f ( Walks ` g ) p /\ ( p ` 0 ) = ( p ` ( # ` f ) ) ) } )
20	0 19	wceq	|- ClWalks = ( g e. _V |-> { <. f , p >. | ( f ( Walks ` g ) p /\ ( p ` 0 ) = ( p ` ( # ` f ) ) ) } )