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 = ( 𝑔 ∈ V ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Walks ‘ 𝑔 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) ) } ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cclwlks | ⊢ ClWalks | |
| 1 | vg | ⊢ 𝑔 | |
| 2 | cvv | ⊢ V | |
| 3 | vf | ⊢ 𝑓 | |
| 4 | vp | ⊢ 𝑝 | |
| 5 | 3 | cv | ⊢ 𝑓 |
| 6 | cwlks | ⊢ Walks | |
| 7 | 1 | cv | ⊢ 𝑔 |
| 8 | 7 6 | cfv | ⊢ ( Walks ‘ 𝑔 ) |
| 9 | 4 | cv | ⊢ 𝑝 |
| 10 | 5 9 8 | wbr | ⊢ 𝑓 ( Walks ‘ 𝑔 ) 𝑝 |
| 11 | cc0 | ⊢ 0 | |
| 12 | 11 9 | cfv | ⊢ ( 𝑝 ‘ 0 ) |
| 13 | chash | ⊢ ♯ | |
| 14 | 5 13 | cfv | ⊢ ( ♯ ‘ 𝑓 ) |
| 15 | 14 9 | cfv | ⊢ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) |
| 16 | 12 15 | wceq | ⊢ ( 𝑝 ‘ 0 ) = ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) |
| 17 | 10 16 | wa | ⊢ ( 𝑓 ( Walks ‘ 𝑔 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) ) |
| 18 | 17 3 4 | copab | ⊢ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Walks ‘ 𝑔 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) ) } |
| 19 | 1 2 18 | cmpt | ⊢ ( 𝑔 ∈ V ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Walks ‘ 𝑔 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) ) } ) |
| 20 | 0 19 | wceq | ⊢ ClWalks = ( 𝑔 ∈ V ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Walks ‘ 𝑔 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) ) } ) |