Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-clwwlksn Structured version   Visualization version   GIF version

Definition df-clwwlksn 41186
 Description: Define the set of all closed walks (in an undirected graph) of a fixed length n as words over the set of vertices. 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 40977. (Contributed by Alexander van der Vekens, 20-Mar-2018.) (Revised by AV, 24-Apr-2021.)
Assertion
Ref Expression
df-clwwlksn ClWWalkSN = (𝑛 ∈ ℕ, 𝑔 ∈ V ↦ {𝑤 ∈ (ClWWalkS‘𝑔) ∣ (#‘𝑤) = 𝑛})
Distinct variable group:   𝑔,𝑛,𝑤

Detailed syntax breakdown of Definition df-clwwlksn
StepHypRef Expression
1 cclwwlksn 41184 . 2 class ClWWalkSN
2 vn . . 3 setvar 𝑛
3 vg . . 3 setvar 𝑔
4 cn 10897 . . 3 class
5 cvv 3173 . . 3 class V
6 vw . . . . . . 7 setvar 𝑤
76cv 1474 . . . . . 6 class 𝑤
8 chash 12979 . . . . . 6 class #
97, 8cfv 5804 . . . . 5 class (#‘𝑤)
102cv 1474 . . . . 5 class 𝑛
119, 10wceq 1475 . . . 4 wff (#‘𝑤) = 𝑛
123cv 1474 . . . . 5 class 𝑔
13 cclwwlks 41183 . . . . 5 class ClWWalkS
1412, 13cfv 5804 . . . 4 class (ClWWalkS‘𝑔)
1511, 6, 14crab 2900 . . 3 class {𝑤 ∈ (ClWWalkS‘𝑔) ∣ (#‘𝑤) = 𝑛}
162, 3, 4, 5, 15cmpt2 6551 . 2 class (𝑛 ∈ ℕ, 𝑔 ∈ V ↦ {𝑤 ∈ (ClWWalkS‘𝑔) ∣ (#‘𝑤) = 𝑛})
171, 16wceq 1475 1 wff ClWWalkSN = (𝑛 ∈ ℕ, 𝑔 ∈ V ↦ {𝑤 ∈ (ClWWalkS‘𝑔) ∣ (#‘𝑤) = 𝑛})
 Colors of variables: wff setvar class This definition is referenced by:  clwwlksn  41189  clwwlknbp0  41192
 Copyright terms: Public domain W3C validator