![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-clwwlkn | Structured version Visualization version GIF version |
Description: Define the set of all closed walks of a fixed length π as words over the set of vertices in a graph π. If 0 < π, such a word corresponds to the sequence p(0) p(1) ... p(n-1) of the vertices in a closed walk p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n)=p(0) as defined in df-clwlks 28768. For π = 0, the set is empty, see clwwlkn0 29021. (Contributed by Alexander van der Vekens, 20-Mar-2018.) (Revised by AV, 24-Apr-2021.) (Revised by AV, 22-Mar-2022.) |
Ref | Expression |
---|---|
df-clwwlkn | β’ ClWWalksN = (π β β0, π β V β¦ {π€ β (ClWWalksβπ) β£ (β―βπ€) = π}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cclwwlkn 29017 | . 2 class ClWWalksN | |
2 | vn | . . 3 setvar π | |
3 | vg | . . 3 setvar π | |
4 | cn0 12421 | . . 3 class β0 | |
5 | cvv 3447 | . . 3 class V | |
6 | vw | . . . . . . 7 setvar π€ | |
7 | 6 | cv 1541 | . . . . . 6 class π€ |
8 | chash 14239 | . . . . . 6 class β― | |
9 | 7, 8 | cfv 6500 | . . . . 5 class (β―βπ€) |
10 | 2 | cv 1541 | . . . . 5 class π |
11 | 9, 10 | wceq 1542 | . . . 4 wff (β―βπ€) = π |
12 | 3 | cv 1541 | . . . . 5 class π |
13 | cclwwlk 28974 | . . . . 5 class ClWWalks | |
14 | 12, 13 | cfv 6500 | . . . 4 class (ClWWalksβπ) |
15 | 11, 6, 14 | crab 3406 | . . 3 class {π€ β (ClWWalksβπ) β£ (β―βπ€) = π} |
16 | 2, 3, 4, 5, 15 | cmpo 7363 | . 2 class (π β β0, π β V β¦ {π€ β (ClWWalksβπ) β£ (β―βπ€) = π}) |
17 | 1, 16 | wceq 1542 | 1 wff ClWWalksN = (π β β0, π β V β¦ {π€ β (ClWWalksβπ) β£ (β―βπ€) = π}) |
Colors of variables: wff setvar class |
This definition is referenced by: clwwlkn 29019 clwwlkneq0 29022 |
Copyright terms: Public domain | W3C validator |