![]() |
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 pseudographs 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 46121 | . 2 class UPWalks | |
2 | vg | . . 3 setvar 𝑔 | |
3 | cvv 3444 | . . 3 class V | |
4 | vf | . . . . . . 7 setvar 𝑓 | |
5 | 4 | cv 1541 | . . . . . 6 class 𝑓 |
6 | 2 | cv 1541 | . . . . . . . . 9 class 𝑔 |
7 | ciedg 27990 | . . . . . . . . 9 class iEdg | |
8 | 6, 7 | cfv 6497 | . . . . . . . 8 class (iEdg‘𝑔) |
9 | 8 | cdm 5634 | . . . . . . 7 class dom (iEdg‘𝑔) |
10 | 9 | cword 14408 | . . . . . 6 class Word dom (iEdg‘𝑔) |
11 | 5, 10 | wcel 2107 | . . . . 5 wff 𝑓 ∈ Word dom (iEdg‘𝑔) |
12 | cc0 11056 | . . . . . . 7 class 0 | |
13 | chash 14236 | . . . . . . . 8 class ♯ | |
14 | 5, 13 | cfv 6497 | . . . . . . 7 class (♯‘𝑓) |
15 | cfz 13430 | . . . . . . 7 class ... | |
16 | 12, 14, 15 | co 7358 | . . . . . 6 class (0...(♯‘𝑓)) |
17 | cvtx 27989 | . . . . . . 7 class Vtx | |
18 | 6, 17 | cfv 6497 | . . . . . 6 class (Vtx‘𝑔) |
19 | vp | . . . . . . 7 setvar 𝑝 | |
20 | 19 | cv 1541 | . . . . . 6 class 𝑝 |
21 | 16, 18, 20 | wf 6493 | . . . . 5 wff 𝑝:(0...(♯‘𝑓))⟶(Vtx‘𝑔) |
22 | vk | . . . . . . . . . 10 setvar 𝑘 | |
23 | 22 | cv 1541 | . . . . . . . . 9 class 𝑘 |
24 | 23, 5 | cfv 6497 | . . . . . . . 8 class (𝑓‘𝑘) |
25 | 24, 8 | cfv 6497 | . . . . . . 7 class ((iEdg‘𝑔)‘(𝑓‘𝑘)) |
26 | 23, 20 | cfv 6497 | . . . . . . . 8 class (𝑝‘𝑘) |
27 | c1 11057 | . . . . . . . . . 10 class 1 | |
28 | caddc 11059 | . . . . . . . . . 10 class + | |
29 | 23, 27, 28 | co 7358 | . . . . . . . . 9 class (𝑘 + 1) |
30 | 29, 20 | cfv 6497 | . . . . . . . 8 class (𝑝‘(𝑘 + 1)) |
31 | 26, 30 | cpr 4589 | . . . . . . 7 class {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} |
32 | 25, 31 | wceq 1542 | . . . . . 6 wff ((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} |
33 | cfzo 13573 | . . . . . . 7 class ..^ | |
34 | 12, 14, 33 | co 7358 | . . . . . 6 class (0..^(♯‘𝑓)) |
35 | 32, 22, 34 | wral 3061 | . . . . 5 wff ∀𝑘 ∈ (0..^(♯‘𝑓))((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} |
36 | 11, 21, 35 | w3a 1088 | . . . 4 wff (𝑓 ∈ Word dom (iEdg‘𝑔) ∧ 𝑝:(0...(♯‘𝑓))⟶(Vtx‘𝑔) ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))}) |
37 | 36, 4, 19 | copab 5168 | . . 3 class {⟨𝑓, 𝑝⟩ ∣ (𝑓 ∈ Word dom (iEdg‘𝑔) ∧ 𝑝:(0...(♯‘𝑓))⟶(Vtx‘𝑔) ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})} |
38 | 2, 3, 37 | cmpt 5189 | . 2 class (𝑔 ∈ V ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓 ∈ Word dom (iEdg‘𝑔) ∧ 𝑝:(0...(♯‘𝑓))⟶(Vtx‘𝑔) ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})}) |
39 | 1, 38 | wceq 1542 | 1 wff UPWalks = (𝑔 ∈ V ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓 ∈ Word dom (iEdg‘𝑔) ∧ 𝑝:(0...(♯‘𝑓))⟶(Vtx‘𝑔) ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})}) |
Colors of variables: wff setvar class |
This definition is referenced by: upwlksfval 46123 |
Copyright terms: Public domain | W3C validator |