Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-wlk Unicode version

Definition df-wlk 28318
Description: Define the set of all Walks (in an undirected graph).

According to Wikipedia ("Path (graph theory)", https://en.wikipedia.org/wiki/Path_(graph_theory), 3-Oct-2017): "A walk of length k in a graph is an alternating sequence of vertices and edges, v0 , e0 , v1 , e1 , v2 , ... , v(k-1) , e(k-1) , v(k) which begins and ends with vertices. If the graph is undirected, then the endpoints of e(i) are v(i) and v(i+1)."

According to Bollobas: " A walk W in a graph is an alternating sequence of vertices and edges x0 , e1 , x1 , e2 , ... , e(l) , x(l) where e(i) = x(i-1)x(i), 0<i<=l.", see Definition of [Bollobas] p. 4.

Therefore, a walk can be represented by two mappings f from { 1 , ... , n } and p from { 0 , ... , n }, where f enumerates the (indices of the) edges, and p enumerates the vertices. So the walk is represented by the following sequence: p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n). (Contributed by Alexander van der Vekens and Mario Carneiro, 4-Oct-2017.)

Assertion
Ref Expression
df-wlk  |- Walks  =  ( v  e.  _V , 
e  e.  _V  |->  {
<. f ,  p >.  |  ( f  e. Word  dom  e  /\  p : ( 0 ... ( # `  f ) ) --> v  /\  A. k  e.  ( 0..^ ( # `  f ) ) ( e `  ( f `
 k ) )  =  { ( p `
 k ) ,  ( p `  (
k  +  1 ) ) } ) } )
Distinct variable group:    v, e, k, f, p

Detailed syntax breakdown of Definition df-wlk
StepHypRef Expression
1 cwalk 28309 . 2  class Walks
2 vv . . 3  set  v
3 ve . . 3  set  e
4 cvv 2801 . . 3  class  _V
5 vf . . . . . . 7  set  f
65cv 1631 . . . . . 6  class  f
73cv 1631 . . . . . . . 8  class  e
87cdm 4705 . . . . . . 7  class  dom  e
98cword 11419 . . . . . 6  class Word  dom  e
106, 9wcel 1696 . . . . 5  wff  f  e. Word  dom  e
11 cc0 8753 . . . . . . 7  class  0
12 chash 11353 . . . . . . . 8  class  #
136, 12cfv 5271 . . . . . . 7  class  ( # `  f )
14 cfz 10798 . . . . . . 7  class  ...
1511, 13, 14co 5874 . . . . . 6  class  ( 0 ... ( # `  f
) )
162cv 1631 . . . . . 6  class  v
17 vp . . . . . . 7  set  p
1817cv 1631 . . . . . 6  class  p
1915, 16, 18wf 5267 . . . . 5  wff  p : ( 0 ... ( # `
 f ) ) --> v
20 vk . . . . . . . . . 10  set  k
2120cv 1631 . . . . . . . . 9  class  k
2221, 6cfv 5271 . . . . . . . 8  class  ( f `
 k )
2322, 7cfv 5271 . . . . . . 7  class  ( e `
 ( f `  k ) )
2421, 18cfv 5271 . . . . . . . 8  class  ( p `
 k )
25 c1 8754 . . . . . . . . . 10  class  1
26 caddc 8756 . . . . . . . . . 10  class  +
2721, 25, 26co 5874 . . . . . . . . 9  class  ( k  +  1 )
2827, 18cfv 5271 . . . . . . . 8  class  ( p `
 ( k  +  1 ) )
2924, 28cpr 3654 . . . . . . 7  class  { ( p `  k ) ,  ( p `  ( k  +  1 ) ) }
3023, 29wceq 1632 . . . . . 6  wff  ( e `
 ( f `  k ) )  =  { ( p `  k ) ,  ( p `  ( k  +  1 ) ) }
31 cfzo 10886 . . . . . . 7  class ..^
3211, 13, 31co 5874 . . . . . 6  class  ( 0..^ ( # `  f
) )
3330, 20, 32wral 2556 . . . . 5  wff  A. k  e.  ( 0..^ ( # `  f ) ) ( e `  ( f `
 k ) )  =  { ( p `
 k ) ,  ( p `  (
k  +  1 ) ) }
3410, 19, 33w3a 934 . . . 4  wff  ( f  e. Word  dom  e  /\  p : ( 0 ... ( # `  f
) ) --> v  /\  A. k  e.  ( 0..^ ( # `  f
) ) ( e `
 ( f `  k ) )  =  { ( p `  k ) ,  ( p `  ( k  +  1 ) ) } )
3534, 5, 17copab 4092 . . 3  class  { <. f ,  p >.  |  ( f  e. Word  dom  e  /\  p : ( 0 ... ( # `  f
) ) --> v  /\  A. k  e.  ( 0..^ ( # `  f
) ) ( e `
 ( f `  k ) )  =  { ( p `  k ) ,  ( p `  ( k  +  1 ) ) } ) }
362, 3, 4, 4, 35cmpt2 5876 . 2  class  ( v  e.  _V ,  e  e.  _V  |->  { <. f ,  p >.  |  ( f  e. Word  dom  e  /\  p : ( 0 ... ( # `  f
) ) --> v  /\  A. k  e.  ( 0..^ ( # `  f
) ) ( e `
 ( f `  k ) )  =  { ( p `  k ) ,  ( p `  ( k  +  1 ) ) } ) } )
371, 36wceq 1632 1  wff Walks  =  ( v  e.  _V , 
e  e.  _V  |->  {
<. f ,  p >.  |  ( f  e. Word  dom  e  /\  p : ( 0 ... ( # `  f ) ) --> v  /\  A. k  e.  ( 0..^ ( # `  f ) ) ( e `  ( f `
 k ) )  =  { ( p `
 k ) ,  ( p `  (
k  +  1 ) ) } ) } )
Colors of variables: wff set class
This definition is referenced by:  wlks  28327  2mwlk  28329  wlkbprop  28332  wlkdvspth  28365
  Copyright terms: Public domain W3C validator