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 |
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.) |
Ref | Expression |
---|---|
df-upwlks | ⊢ UPWalks = (𝑔 ∈ V ↦ {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom (iEdg‘𝑔) ∧ 𝑝:(0...(#‘𝑓))⟶(Vtx‘𝑔) ∧ ∀𝑘 ∈ (0..^(#‘𝑓))((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cupwlks 41714 | . 2 class UPWalks | |
2 | vg | . . 3 setvar 𝑔 | |
3 | cvv 3200 | . . 3 class V | |
4 | vf | . . . . . . 7 setvar 𝑓 | |
5 | 4 | cv 1482 | . . . . . 6 class 𝑓 |
6 | 2 | cv 1482 | . . . . . . . . 9 class 𝑔 |
7 | ciedg 25875 | . . . . . . . . 9 class iEdg | |
8 | 6, 7 | cfv 5888 | . . . . . . . 8 class (iEdg‘𝑔) |
9 | 8 | cdm 5114 | . . . . . . 7 class dom (iEdg‘𝑔) |
10 | 9 | cword 13291 | . . . . . 6 class Word dom (iEdg‘𝑔) |
11 | 5, 10 | wcel 1990 | . . . . 5 wff 𝑓 ∈ Word dom (iEdg‘𝑔) |
12 | cc0 9936 | . . . . . . 7 class 0 | |
13 | chash 13117 | . . . . . . . 8 class # | |
14 | 5, 13 | cfv 5888 | . . . . . . 7 class (#‘𝑓) |
15 | cfz 12326 | . . . . . . 7 class ... | |
16 | 12, 14, 15 | co 6650 | . . . . . 6 class (0...(#‘𝑓)) |
17 | cvtx 25874 | . . . . . . 7 class Vtx | |
18 | 6, 17 | cfv 5888 | . . . . . 6 class (Vtx‘𝑔) |
19 | vp | . . . . . . 7 setvar 𝑝 | |
20 | 19 | cv 1482 | . . . . . 6 class 𝑝 |
21 | 16, 18, 20 | wf 5884 | . . . . 5 wff 𝑝:(0...(#‘𝑓))⟶(Vtx‘𝑔) |
22 | vk | . . . . . . . . . 10 setvar 𝑘 | |
23 | 22 | cv 1482 | . . . . . . . . 9 class 𝑘 |
24 | 23, 5 | cfv 5888 | . . . . . . . 8 class (𝑓‘𝑘) |
25 | 24, 8 | cfv 5888 | . . . . . . 7 class ((iEdg‘𝑔)‘(𝑓‘𝑘)) |
26 | 23, 20 | cfv 5888 | . . . . . . . 8 class (𝑝‘𝑘) |
27 | c1 9937 | . . . . . . . . . 10 class 1 | |
28 | caddc 9939 | . . . . . . . . . 10 class + | |
29 | 23, 27, 28 | co 6650 | . . . . . . . . 9 class (𝑘 + 1) |
30 | 29, 20 | cfv 5888 | . . . . . . . 8 class (𝑝‘(𝑘 + 1)) |
31 | 26, 30 | cpr 4179 | . . . . . . 7 class {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} |
32 | 25, 31 | wceq 1483 | . . . . . 6 wff ((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} |
33 | cfzo 12465 | . . . . . . 7 class ..^ | |
34 | 12, 14, 33 | co 6650 | . . . . . 6 class (0..^(#‘𝑓)) |
35 | 32, 22, 34 | wral 2912 | . . . . 5 wff ∀𝑘 ∈ (0..^(#‘𝑓))((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} |
36 | 11, 21, 35 | w3a 1037 | . . . 4 wff (𝑓 ∈ Word dom (iEdg‘𝑔) ∧ 𝑝:(0...(#‘𝑓))⟶(Vtx‘𝑔) ∧ ∀𝑘 ∈ (0..^(#‘𝑓))((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))}) |
37 | 36, 4, 19 | copab 4712 | . . 3 class {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom (iEdg‘𝑔) ∧ 𝑝:(0...(#‘𝑓))⟶(Vtx‘𝑔) ∧ ∀𝑘 ∈ (0..^(#‘𝑓))((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})} |
38 | 2, 3, 37 | cmpt 4729 | . 2 class (𝑔 ∈ V ↦ {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom (iEdg‘𝑔) ∧ 𝑝:(0...(#‘𝑓))⟶(Vtx‘𝑔) ∧ ∀𝑘 ∈ (0..^(#‘𝑓))((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})}) |
39 | 1, 38 | wceq 1483 | 1 wff UPWalks = (𝑔 ∈ V ↦ {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom (iEdg‘𝑔) ∧ 𝑝:(0...(#‘𝑓))⟶(Vtx‘𝑔) ∧ ∀𝑘 ∈ (0..^(#‘𝑓))((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})}) |
Colors of variables: wff setvar class |
This definition is referenced by: upwlksfval 41716 |
Copyright terms: Public domain | W3C validator |