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

Definition df-wlks 40793
Description: Define the set of all walks (in a pseudograph). TODO-AV: This corresponds to the definition of Walks, but can be removed and the defining theorem upgriswlk 40841 could be used instead.

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).

Although this definition is also applicable for arbitrary hypergraphs, it allows only walks consisting of not proper hyperedges (i.e. edges connecting at most two vertices). Therefore, it should be used for pseudograhs only. (Contributed by Alexander van der Vekens and Mario Carneiro, 4-Oct-2017.) (Revised by AV, 28-Dec-2020.)

Assertion
Ref Expression
df-wlks UPWalks = (𝑔 ∈ V ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓 ∈ Word dom (iEdg‘𝑔) ∧ 𝑝:(0...(#‘𝑓))⟶(Vtx‘𝑔) ∧ ∀𝑘 ∈ (0..^(#‘𝑓))((iEdg‘𝑔)‘(𝑓𝑘)) = {(𝑝𝑘), (𝑝‘(𝑘 + 1))})})
Distinct variable group:   𝑓,𝑔,𝑘,𝑝

Detailed syntax breakdown of Definition df-wlks
StepHypRef Expression
1 cwlks 40789 . 2 class UPWalks
2 vg . . 3 setvar 𝑔
3 cvv 3173 . . 3 class V
4 vf . . . . . . 7 setvar 𝑓
54cv 1474 . . . . . 6 class 𝑓
62cv 1474 . . . . . . . . 9 class 𝑔
7 ciedg 40222 . . . . . . . . 9 class iEdg
86, 7cfv 5790 . . . . . . . 8 class (iEdg‘𝑔)
98cdm 5028 . . . . . . 7 class dom (iEdg‘𝑔)
109cword 13095 . . . . . 6 class Word dom (iEdg‘𝑔)
115, 10wcel 1977 . . . . 5 wff 𝑓 ∈ Word dom (iEdg‘𝑔)
12 cc0 9793 . . . . . . 7 class 0
13 chash 12937 . . . . . . . 8 class #
145, 13cfv 5790 . . . . . . 7 class (#‘𝑓)
15 cfz 12155 . . . . . . 7 class ...
1612, 14, 15co 6527 . . . . . 6 class (0...(#‘𝑓))
17 cvtx 40221 . . . . . . 7 class Vtx
186, 17cfv 5790 . . . . . 6 class (Vtx‘𝑔)
19 vp . . . . . . 7 setvar 𝑝
2019cv 1474 . . . . . 6 class 𝑝
2116, 18, 20wf 5786 . . . . 5 wff 𝑝:(0...(#‘𝑓))⟶(Vtx‘𝑔)
22 vk . . . . . . . . . 10 setvar 𝑘
2322cv 1474 . . . . . . . . 9 class 𝑘
2423, 5cfv 5790 . . . . . . . 8 class (𝑓𝑘)
2524, 8cfv 5790 . . . . . . 7 class ((iEdg‘𝑔)‘(𝑓𝑘))
2623, 20cfv 5790 . . . . . . . 8 class (𝑝𝑘)
27 c1 9794 . . . . . . . . . 10 class 1
28 caddc 9796 . . . . . . . . . 10 class +
2923, 27, 28co 6527 . . . . . . . . 9 class (𝑘 + 1)
3029, 20cfv 5790 . . . . . . . 8 class (𝑝‘(𝑘 + 1))
3126, 30cpr 4127 . . . . . . 7 class {(𝑝𝑘), (𝑝‘(𝑘 + 1))}
3225, 31wceq 1475 . . . . . 6 wff ((iEdg‘𝑔)‘(𝑓𝑘)) = {(𝑝𝑘), (𝑝‘(𝑘 + 1))}
33 cfzo 12292 . . . . . . 7 class ..^
3412, 14, 33co 6527 . . . . . 6 class (0..^(#‘𝑓))
3532, 22, 34wral 2896 . . . . 5 wff 𝑘 ∈ (0..^(#‘𝑓))((iEdg‘𝑔)‘(𝑓𝑘)) = {(𝑝𝑘), (𝑝‘(𝑘 + 1))}
3611, 21, 35w3a 1031 . . . 4 wff (𝑓 ∈ Word dom (iEdg‘𝑔) ∧ 𝑝:(0...(#‘𝑓))⟶(Vtx‘𝑔) ∧ ∀𝑘 ∈ (0..^(#‘𝑓))((iEdg‘𝑔)‘(𝑓𝑘)) = {(𝑝𝑘), (𝑝‘(𝑘 + 1))})
3736, 4, 19copab 4637 . . 3 class {⟨𝑓, 𝑝⟩ ∣ (𝑓 ∈ Word dom (iEdg‘𝑔) ∧ 𝑝:(0...(#‘𝑓))⟶(Vtx‘𝑔) ∧ ∀𝑘 ∈ (0..^(#‘𝑓))((iEdg‘𝑔)‘(𝑓𝑘)) = {(𝑝𝑘), (𝑝‘(𝑘 + 1))})}
382, 3, 37cmpt 4638 . 2 class (𝑔 ∈ V ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓 ∈ Word dom (iEdg‘𝑔) ∧ 𝑝:(0...(#‘𝑓))⟶(Vtx‘𝑔) ∧ ∀𝑘 ∈ (0..^(#‘𝑓))((iEdg‘𝑔)‘(𝑓𝑘)) = {(𝑝𝑘), (𝑝‘(𝑘 + 1))})})
391, 38wceq 1475 1 wff UPWalks = (𝑔 ∈ V ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓 ∈ Word dom (iEdg‘𝑔) ∧ 𝑝:(0...(#‘𝑓))⟶(Vtx‘𝑔) ∧ ∀𝑘 ∈ (0..^(#‘𝑓))((iEdg‘𝑔)‘(𝑓𝑘)) = {(𝑝𝑘), (𝑝‘(𝑘 + 1))})})
Colors of variables: wff setvar class
This definition is referenced by:  wlksfval  40804
  Copyright terms: Public domain W3C validator