Metamath Proof Explorer


Definition df-ewlks

Description: Define the set of all s-walks of edges (in a hypergraph) corresponding to s-walks "on the edge level" discussed in Aksoy et al. For an extended nonnegative integer s, an s-walk is a sequence of hyperedges, e(0), e(1), ... , e(k), where e(j-1) and e(j) have at least s vertices in common (for j=1, ... , k). In contrast to the definition in Aksoy et al., s = 0 (a 0-walk is an arbitrary sequence of hyperedges) and s = +oo (then the number of common vertices of two adjacent hyperedges must be infinite) are allowed. Furthermore, it is not forbidden that adjacent hyperedges are equal. (Contributed by AV, 4-Jan-2021)

Ref Expression
Assertion df-ewlks
|- EdgWalks = ( g e. _V , s e. NN0* |-> { f | [. ( iEdg ` g ) / i ]. ( f e. Word dom i /\ A. k e. ( 1 ..^ ( # ` f ) ) s <_ ( # ` ( ( i ` ( f ` ( k - 1 ) ) ) i^i ( i ` ( f ` k ) ) ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cewlks
 |-  EdgWalks
1 vg
 |-  g
2 cvv
 |-  _V
3 vs
 |-  s
4 cxnn0
 |-  NN0*
5 vf
 |-  f
6 ciedg
 |-  iEdg
7 1 cv
 |-  g
8 7 6 cfv
 |-  ( iEdg ` g )
9 vi
 |-  i
10 5 cv
 |-  f
11 9 cv
 |-  i
12 11 cdm
 |-  dom i
13 12 cword
 |-  Word dom i
14 10 13 wcel
 |-  f e. Word dom i
15 vk
 |-  k
16 c1
 |-  1
17 cfzo
 |-  ..^
18 chash
 |-  #
19 10 18 cfv
 |-  ( # ` f )
20 16 19 17 co
 |-  ( 1 ..^ ( # ` f ) )
21 3 cv
 |-  s
22 cle
 |-  <_
23 15 cv
 |-  k
24 cmin
 |-  -
25 23 16 24 co
 |-  ( k - 1 )
26 25 10 cfv
 |-  ( f ` ( k - 1 ) )
27 26 11 cfv
 |-  ( i ` ( f ` ( k - 1 ) ) )
28 23 10 cfv
 |-  ( f ` k )
29 28 11 cfv
 |-  ( i ` ( f ` k ) )
30 27 29 cin
 |-  ( ( i ` ( f ` ( k - 1 ) ) ) i^i ( i ` ( f ` k ) ) )
31 30 18 cfv
 |-  ( # ` ( ( i ` ( f ` ( k - 1 ) ) ) i^i ( i ` ( f ` k ) ) ) )
32 21 31 22 wbr
 |-  s <_ ( # ` ( ( i ` ( f ` ( k - 1 ) ) ) i^i ( i ` ( f ` k ) ) ) )
33 32 15 20 wral
 |-  A. k e. ( 1 ..^ ( # ` f ) ) s <_ ( # ` ( ( i ` ( f ` ( k - 1 ) ) ) i^i ( i ` ( f ` k ) ) ) )
34 14 33 wa
 |-  ( f e. Word dom i /\ A. k e. ( 1 ..^ ( # ` f ) ) s <_ ( # ` ( ( i ` ( f ` ( k - 1 ) ) ) i^i ( i ` ( f ` k ) ) ) ) )
35 34 9 8 wsbc
 |-  [. ( iEdg ` g ) / i ]. ( f e. Word dom i /\ A. k e. ( 1 ..^ ( # ` f ) ) s <_ ( # ` ( ( i ` ( f ` ( k - 1 ) ) ) i^i ( i ` ( f ` k ) ) ) ) )
36 35 5 cab
 |-  { f | [. ( iEdg ` g ) / i ]. ( f e. Word dom i /\ A. k e. ( 1 ..^ ( # ` f ) ) s <_ ( # ` ( ( i ` ( f ` ( k - 1 ) ) ) i^i ( i ` ( f ` k ) ) ) ) ) }
37 1 3 2 4 36 cmpo
 |-  ( g e. _V , s e. NN0* |-> { f | [. ( iEdg ` g ) / i ]. ( f e. Word dom i /\ A. k e. ( 1 ..^ ( # ` f ) ) s <_ ( # ` ( ( i ` ( f ` ( k - 1 ) ) ) i^i ( i ` ( f ` k ) ) ) ) ) } )
38 0 37 wceq
 |-  EdgWalks = ( g e. _V , s e. NN0* |-> { f | [. ( iEdg ` g ) / i ]. ( f e. Word dom i /\ A. k e. ( 1 ..^ ( # ` f ) ) s <_ ( # ` ( ( i ` ( f ` ( k - 1 ) ) ) i^i ( i ` ( f ` k ) ) ) ) ) } )