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 47977
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 pseudographs 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 47976 . 2 class UPWalks
2 vg . . 3 setvar 𝑔
3 cvv 3477 . . 3 class V
4 vf . . . . . . 7 setvar 𝑓
54cv 1535 . . . . . 6 class 𝑓
62cv 1535 . . . . . . . . 9 class 𝑔
7 ciedg 29028 . . . . . . . . 9 class iEdg
86, 7cfv 6562 . . . . . . . 8 class (iEdg‘𝑔)
98cdm 5688 . . . . . . 7 class dom (iEdg‘𝑔)
109cword 14548 . . . . . 6 class Word dom (iEdg‘𝑔)
115, 10wcel 2105 . . . . 5 wff 𝑓 ∈ Word dom (iEdg‘𝑔)
12 cc0 11152 . . . . . . 7 class 0
13 chash 14365 . . . . . . . 8 class
145, 13cfv 6562 . . . . . . 7 class (♯‘𝑓)
15 cfz 13543 . . . . . . 7 class ...
1612, 14, 15co 7430 . . . . . 6 class (0...(♯‘𝑓))
17 cvtx 29027 . . . . . . 7 class Vtx
186, 17cfv 6562 . . . . . 6 class (Vtx‘𝑔)
19 vp . . . . . . 7 setvar 𝑝
2019cv 1535 . . . . . 6 class 𝑝
2116, 18, 20wf 6558 . . . . 5 wff 𝑝:(0...(♯‘𝑓))⟶(Vtx‘𝑔)
22 vk . . . . . . . . . 10 setvar 𝑘
2322cv 1535 . . . . . . . . 9 class 𝑘
2423, 5cfv 6562 . . . . . . . 8 class (𝑓𝑘)
2524, 8cfv 6562 . . . . . . 7 class ((iEdg‘𝑔)‘(𝑓𝑘))
2623, 20cfv 6562 . . . . . . . 8 class (𝑝𝑘)
27 c1 11153 . . . . . . . . . 10 class 1
28 caddc 11155 . . . . . . . . . 10 class +
2923, 27, 28co 7430 . . . . . . . . 9 class (𝑘 + 1)
3029, 20cfv 6562 . . . . . . . 8 class (𝑝‘(𝑘 + 1))
3126, 30cpr 4632 . . . . . . 7 class {(𝑝𝑘), (𝑝‘(𝑘 + 1))}
3225, 31wceq 1536 . . . . . 6 wff ((iEdg‘𝑔)‘(𝑓𝑘)) = {(𝑝𝑘), (𝑝‘(𝑘 + 1))}
33 cfzo 13690 . . . . . . 7 class ..^
3412, 14, 33co 7430 . . . . . 6 class (0..^(♯‘𝑓))
3532, 22, 34wral 3058 . . . . 5 wff 𝑘 ∈ (0..^(♯‘𝑓))((iEdg‘𝑔)‘(𝑓𝑘)) = {(𝑝𝑘), (𝑝‘(𝑘 + 1))}
3611, 21, 35w3a 1086 . . . 4 wff (𝑓 ∈ Word dom (iEdg‘𝑔) ∧ 𝑝:(0...(♯‘𝑓))⟶(Vtx‘𝑔) ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))((iEdg‘𝑔)‘(𝑓𝑘)) = {(𝑝𝑘), (𝑝‘(𝑘 + 1))})
3736, 4, 19copab 5209 . . 3 class {⟨𝑓, 𝑝⟩ ∣ (𝑓 ∈ Word dom (iEdg‘𝑔) ∧ 𝑝:(0...(♯‘𝑓))⟶(Vtx‘𝑔) ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))((iEdg‘𝑔)‘(𝑓𝑘)) = {(𝑝𝑘), (𝑝‘(𝑘 + 1))})}
382, 3, 37cmpt 5230 . 2 class (𝑔 ∈ V ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓 ∈ Word dom (iEdg‘𝑔) ∧ 𝑝:(0...(♯‘𝑓))⟶(Vtx‘𝑔) ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))((iEdg‘𝑔)‘(𝑓𝑘)) = {(𝑝𝑘), (𝑝‘(𝑘 + 1))})})
391, 38wceq 1536 1 wff UPWalks = (𝑔 ∈ V ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓 ∈ Word dom (iEdg‘𝑔) ∧ 𝑝:(0...(♯‘𝑓))⟶(Vtx‘𝑔) ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))((iEdg‘𝑔)‘(𝑓𝑘)) = {(𝑝𝑘), (𝑝‘(𝑘 + 1))})})
Colors of variables: wff setvar class
This definition is referenced by:  upwlksfval  47978
  Copyright terms: Public domain W3C validator