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

Definition df-upwlks 42243
Description: Define the set of all walks (in a pseudograph), called "simple walks" in the following.

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-upwlks UPWalks = (𝑔 ∈ V ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓 ∈ Word dom (iEdg‘𝑔) ∧ 𝑝:(0...(♯‘𝑓))⟶(Vtx‘𝑔) ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))((iEdg‘𝑔)‘(𝑓𝑘)) = {(𝑝𝑘), (𝑝‘(𝑘 + 1))})})
Distinct variable group:   𝑓,𝑔,𝑘,𝑝

Detailed syntax breakdown of Definition df-upwlks
StepHypRef Expression
1 cupwlks 42242 . 2 class UPWalks
2 vg . . 3 setvar 𝑔
3 cvv 3340 . . 3 class V
4 vf . . . . . . 7 setvar 𝑓
54cv 1631 . . . . . 6 class 𝑓
62cv 1631 . . . . . . . . 9 class 𝑔
7 ciedg 26095 . . . . . . . . 9 class iEdg
86, 7cfv 6049 . . . . . . . 8 class (iEdg‘𝑔)
98cdm 5266 . . . . . . 7 class dom (iEdg‘𝑔)
109cword 13497 . . . . . 6 class Word dom (iEdg‘𝑔)
115, 10wcel 2139 . . . . 5 wff 𝑓 ∈ Word dom (iEdg‘𝑔)
12 cc0 10148 . . . . . . 7 class 0
13 chash 13331 . . . . . . . 8 class
145, 13cfv 6049 . . . . . . 7 class (♯‘𝑓)
15 cfz 12539 . . . . . . 7 class ...
1612, 14, 15co 6814 . . . . . 6 class (0...(♯‘𝑓))
17 cvtx 26094 . . . . . . 7 class Vtx
186, 17cfv 6049 . . . . . 6 class (Vtx‘𝑔)
19 vp . . . . . . 7 setvar 𝑝
2019cv 1631 . . . . . 6 class 𝑝
2116, 18, 20wf 6045 . . . . 5 wff 𝑝:(0...(♯‘𝑓))⟶(Vtx‘𝑔)
22 vk . . . . . . . . . 10 setvar 𝑘
2322cv 1631 . . . . . . . . 9 class 𝑘
2423, 5cfv 6049 . . . . . . . 8 class (𝑓𝑘)
2524, 8cfv 6049 . . . . . . 7 class ((iEdg‘𝑔)‘(𝑓𝑘))
2623, 20cfv 6049 . . . . . . . 8 class (𝑝𝑘)
27 c1 10149 . . . . . . . . . 10 class 1
28 caddc 10151 . . . . . . . . . 10 class +
2923, 27, 28co 6814 . . . . . . . . 9 class (𝑘 + 1)
3029, 20cfv 6049 . . . . . . . 8 class (𝑝‘(𝑘 + 1))
3126, 30cpr 4323 . . . . . . 7 class {(𝑝𝑘), (𝑝‘(𝑘 + 1))}
3225, 31wceq 1632 . . . . . 6 wff ((iEdg‘𝑔)‘(𝑓𝑘)) = {(𝑝𝑘), (𝑝‘(𝑘 + 1))}
33 cfzo 12679 . . . . . . 7 class ..^
3412, 14, 33co 6814 . . . . . 6 class (0..^(♯‘𝑓))
3532, 22, 34wral 3050 . . . . 5 wff 𝑘 ∈ (0..^(♯‘𝑓))((iEdg‘𝑔)‘(𝑓𝑘)) = {(𝑝𝑘), (𝑝‘(𝑘 + 1))}
3611, 21, 35w3a 1072 . . . 4 wff (𝑓 ∈ Word dom (iEdg‘𝑔) ∧ 𝑝:(0...(♯‘𝑓))⟶(Vtx‘𝑔) ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))((iEdg‘𝑔)‘(𝑓𝑘)) = {(𝑝𝑘), (𝑝‘(𝑘 + 1))})
3736, 4, 19copab 4864 . . 3 class {⟨𝑓, 𝑝⟩ ∣ (𝑓 ∈ Word dom (iEdg‘𝑔) ∧ 𝑝:(0...(♯‘𝑓))⟶(Vtx‘𝑔) ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))((iEdg‘𝑔)‘(𝑓𝑘)) = {(𝑝𝑘), (𝑝‘(𝑘 + 1))})}
382, 3, 37cmpt 4881 . 2 class (𝑔 ∈ V ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓 ∈ Word dom (iEdg‘𝑔) ∧ 𝑝:(0...(♯‘𝑓))⟶(Vtx‘𝑔) ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))((iEdg‘𝑔)‘(𝑓𝑘)) = {(𝑝𝑘), (𝑝‘(𝑘 + 1))})})
391, 38wceq 1632 1 wff UPWalks = (𝑔 ∈ V ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓 ∈ Word dom (iEdg‘𝑔) ∧ 𝑝:(0...(♯‘𝑓))⟶(Vtx‘𝑔) ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))((iEdg‘𝑔)‘(𝑓𝑘)) = {(𝑝𝑘), (𝑝‘(𝑘 + 1))})})
Colors of variables: wff setvar class
This definition is referenced by:  upwlksfval  42244
  Copyright terms: Public domain W3C validator