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

Definition df-clwwlk 30556
Description: Define the set of all Closed Walks (in an undirected graph) as words over the set of vertices. Such a word corresponds to the sequence p(0) p(1) ... p(n-1) of the vertices in a closed walk p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n)=p(0) as defined in df-clwlk 30555. Notice that the word does not contain the terminating vertex p(n) of the walk, because it is always equal to the first vertex of the closed walk.

Notice that by this definition, a single vertex cannot be represented as closed walk, since the word <" v "> with vertex v represents the walk "vv", which is a (closed) walk of length 1 (if there is an edge/loop from v to v). Therefore, a closed walk corresponds to a closed walk as word in an undirected graph only for walks of length at least 1, see clwlkisclwwlk2 30592. (Contributed by Alexander van der Vekens, 20-Mar-2018.)

Assertion
Ref Expression
df-clwwlk  |- ClWWalks  =  ( v  e.  _V , 
e  e.  _V  |->  { w  e. Word  v  |  ( A. i  e.  ( 0..^ ( (
# `  w )  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  e  /\  { ( lastS  `  w
) ,  ( w `
 0 ) }  e.  ran  e ) } )
Distinct variable group:    e, i, v, w

Detailed syntax breakdown of Definition df-clwwlk
StepHypRef Expression
1 cclwwlk 30553 . 2  class ClWWalks
2 vv . . 3  setvar  v
3 ve . . 3  setvar  e
4 cvv 3070 . . 3  class  _V
5 vi . . . . . . . . . 10  setvar  i
65cv 1369 . . . . . . . . 9  class  i
7 vw . . . . . . . . . 10  setvar  w
87cv 1369 . . . . . . . . 9  class  w
96, 8cfv 5518 . . . . . . . 8  class  ( w `
 i )
10 c1 9386 . . . . . . . . . 10  class  1
11 caddc 9388 . . . . . . . . . 10  class  +
126, 10, 11co 6192 . . . . . . . . 9  class  ( i  +  1 )
1312, 8cfv 5518 . . . . . . . 8  class  ( w `
 ( i  +  1 ) )
149, 13cpr 3979 . . . . . . 7  class  { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }
153cv 1369 . . . . . . . 8  class  e
1615crn 4941 . . . . . . 7  class  ran  e
1714, 16wcel 1758 . . . . . 6  wff  { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  e
18 cc0 9385 . . . . . . 7  class  0
19 chash 12206 . . . . . . . . 9  class  #
208, 19cfv 5518 . . . . . . . 8  class  ( # `  w )
21 cmin 9698 . . . . . . . 8  class  -
2220, 10, 21co 6192 . . . . . . 7  class  ( (
# `  w )  -  1 )
23 cfzo 11651 . . . . . . 7  class ..^
2418, 22, 23co 6192 . . . . . 6  class  ( 0..^ ( ( # `  w
)  -  1 ) )
2517, 5, 24wral 2795 . . . . 5  wff  A. i  e.  ( 0..^ ( (
# `  w )  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  e
26 clsw 12326 . . . . . . . 8  class lastS
278, 26cfv 5518 . . . . . . 7  class  ( lastS  `  w
)
2818, 8cfv 5518 . . . . . . 7  class  ( w `
 0 )
2927, 28cpr 3979 . . . . . 6  class  { ( lastS  `  w ) ,  ( w `  0 ) }
3029, 16wcel 1758 . . . . 5  wff  { ( lastS  `  w ) ,  ( w `  0 ) }  e.  ran  e
3125, 30wa 369 . . . 4  wff  ( A. i  e.  ( 0..^ ( ( # `  w
)  -  1 ) ) { ( w `
 i ) ,  ( w `  (
i  +  1 ) ) }  e.  ran  e  /\  { ( lastS  `  w
) ,  ( w `
 0 ) }  e.  ran  e )
322cv 1369 . . . . 5  class  v
3332cword 12325 . . . 4  class Word  v
3431, 7, 33crab 2799 . . 3  class  { w  e. Word  v  |  ( A. i  e.  ( 0..^ ( ( # `  w
)  -  1 ) ) { ( w `
 i ) ,  ( w `  (
i  +  1 ) ) }  e.  ran  e  /\  { ( lastS  `  w
) ,  ( w `
 0 ) }  e.  ran  e ) }
352, 3, 4, 4, 34cmpt2 6194 . 2  class  ( v  e.  _V ,  e  e.  _V  |->  { w  e. Word  v  |  ( A. i  e.  ( 0..^ ( ( # `  w
)  -  1 ) ) { ( w `
 i ) ,  ( w `  (
i  +  1 ) ) }  e.  ran  e  /\  { ( lastS  `  w
) ,  ( w `
 0 ) }  e.  ran  e ) } )
361, 35wceq 1370 1  wff ClWWalks  =  ( v  e.  _V , 
e  e.  _V  |->  { w  e. Word  v  |  ( A. i  e.  ( 0..^ ( (
# `  w )  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  e  /\  { ( lastS  `  w
) ,  ( w `
 0 ) }  e.  ran  e ) } )
Colors of variables: wff setvar class
This definition is referenced by:  clwwlk  30569  clwwlkprop  30573
  Copyright terms: Public domain W3C validator