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 |
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 40849 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.) |
Ref | Expression |
---|---|
df-wlks | ⊢ UPWalks = (𝑔 ∈ V ↦ {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom (iEdg‘𝑔) ∧ 𝑝:(0...(#‘𝑓))⟶(Vtx‘𝑔) ∧ ∀𝑘 ∈ (0..^(#‘𝑓))((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cwlks 40797 | . 2 class UPWalks | |
2 | vg | . . 3 setvar 𝑔 | |
3 | cvv 3173 | . . 3 class V | |
4 | vf | . . . . . . 7 setvar 𝑓 | |
5 | 4 | cv 1474 | . . . . . 6 class 𝑓 |
6 | 2 | cv 1474 | . . . . . . . . 9 class 𝑔 |
7 | ciedg 25674 | . . . . . . . . 9 class iEdg | |
8 | 6, 7 | cfv 5804 | . . . . . . . 8 class (iEdg‘𝑔) |
9 | 8 | cdm 5038 | . . . . . . 7 class dom (iEdg‘𝑔) |
10 | 9 | cword 13146 | . . . . . 6 class Word dom (iEdg‘𝑔) |
11 | 5, 10 | wcel 1977 | . . . . 5 wff 𝑓 ∈ Word dom (iEdg‘𝑔) |
12 | cc0 9815 | . . . . . . 7 class 0 | |
13 | chash 12979 | . . . . . . . 8 class # | |
14 | 5, 13 | cfv 5804 | . . . . . . 7 class (#‘𝑓) |
15 | cfz 12197 | . . . . . . 7 class ... | |
16 | 12, 14, 15 | co 6549 | . . . . . 6 class (0...(#‘𝑓)) |
17 | cvtx 25673 | . . . . . . 7 class Vtx | |
18 | 6, 17 | cfv 5804 | . . . . . 6 class (Vtx‘𝑔) |
19 | vp | . . . . . . 7 setvar 𝑝 | |
20 | 19 | cv 1474 | . . . . . 6 class 𝑝 |
21 | 16, 18, 20 | wf 5800 | . . . . 5 wff 𝑝:(0...(#‘𝑓))⟶(Vtx‘𝑔) |
22 | vk | . . . . . . . . . 10 setvar 𝑘 | |
23 | 22 | cv 1474 | . . . . . . . . 9 class 𝑘 |
24 | 23, 5 | cfv 5804 | . . . . . . . 8 class (𝑓‘𝑘) |
25 | 24, 8 | cfv 5804 | . . . . . . 7 class ((iEdg‘𝑔)‘(𝑓‘𝑘)) |
26 | 23, 20 | cfv 5804 | . . . . . . . 8 class (𝑝‘𝑘) |
27 | c1 9816 | . . . . . . . . . 10 class 1 | |
28 | caddc 9818 | . . . . . . . . . 10 class + | |
29 | 23, 27, 28 | co 6549 | . . . . . . . . 9 class (𝑘 + 1) |
30 | 29, 20 | cfv 5804 | . . . . . . . 8 class (𝑝‘(𝑘 + 1)) |
31 | 26, 30 | cpr 4127 | . . . . . . 7 class {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} |
32 | 25, 31 | wceq 1475 | . . . . . 6 wff ((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} |
33 | cfzo 12334 | . . . . . . 7 class ..^ | |
34 | 12, 14, 33 | co 6549 | . . . . . 6 class (0..^(#‘𝑓)) |
35 | 32, 22, 34 | wral 2896 | . . . . 5 wff ∀𝑘 ∈ (0..^(#‘𝑓))((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} |
36 | 11, 21, 35 | w3a 1031 | . . . 4 wff (𝑓 ∈ Word dom (iEdg‘𝑔) ∧ 𝑝:(0...(#‘𝑓))⟶(Vtx‘𝑔) ∧ ∀𝑘 ∈ (0..^(#‘𝑓))((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))}) |
37 | 36, 4, 19 | copab 4642 | . . 3 class {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom (iEdg‘𝑔) ∧ 𝑝:(0...(#‘𝑓))⟶(Vtx‘𝑔) ∧ ∀𝑘 ∈ (0..^(#‘𝑓))((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})} |
38 | 2, 3, 37 | cmpt 4643 | . 2 class (𝑔 ∈ V ↦ {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom (iEdg‘𝑔) ∧ 𝑝:(0...(#‘𝑓))⟶(Vtx‘𝑔) ∧ ∀𝑘 ∈ (0..^(#‘𝑓))((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})}) |
39 | 1, 38 | wceq 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 40812 |
Copyright terms: Public domain | W3C validator |