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 = g ∈ V ⟼ f p | f Walks ⁡ g p ∧ p ⁡ 0 = p ⁡ f

Detailed syntax breakdown

Step Hyp Ref Expression
0 cclwlks class ClWalks
1 vg setvar g
2 cvv class V
3 vf setvar f
4 vp setvar p
5 3 cv setvar f
6 cwlks class Walks
7 1 cv setvar g
8 7 6 cfv class Walks ⁡ g
9 4 cv setvar p
10 5 9 8 wbr wff f Walks ⁡ g p
11 cc0 class 0
12 11 9 cfv class p ⁡ 0
13 chash class .
14 5 13 cfv class f
15 14 9 cfv class p ⁡ f
16 12 15 wceq wff p ⁡ 0 = p ⁡ f
17 10 16 wa wff f Walks ⁡ g p ∧ p ⁡ 0 = p ⁡ f
18 17 3 4 copab class f p | f Walks ⁡ g p ∧ p ⁡ 0 = p ⁡ f
19 1 2 18 cmpt class g ∈ V ⟼ f p | f Walks ⁡ g p ∧ p ⁡ 0 = p ⁡ f
20 0 19 wceq wff ClWalks = g ∈ V ⟼ f p | f Walks ⁡ g p ∧ p ⁡ 0 = p ⁡ f