![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-cycls | Structured version Visualization version GIF version |
Description: Define the set of all
(simple) cycles (in an undirected graph).
According to Wikipedia ("Cycle (graph theory)", https://en.wikipedia.org/wiki/Cycle_(graph_theory), 3-Oct-2017): "A simple cycle may be defined either as a closed walk with no repetitions of vertices and edges allowed, other than the repetition of the starting and ending vertex." According to Bollobas: "If a walk W = x0 x1 ... x(l) is such that l >= 3, x0=x(l), and the vertices x(i), 0 < i < l, are distinct from each other and x0, then W is said to be a cycle." See Definition of [Bollobas] p. 5. However, since a walk consisting of distinct vertices (except the first and the last vertex) is a path, a cycle can be defined as path whose first and last vertices coincide. So a cycle is represented by the following sequence: p(0) e(f(1)) p(1) ... p(n-1) e(f(n)) p(n)=p(0). (Contributed by Alexander van der Vekens, 3-Oct-2017.) (Revised by AV, 31-Jan-2021.) |
Ref | Expression |
---|---|
df-cycls | β’ Cycles = (π β V β¦ {β¨π, πβ© β£ (π(Pathsβπ)π β§ (πβ0) = (πβ(β―βπ)))}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ccycls 28775 | . 2 class Cycles | |
2 | vg | . . 3 setvar π | |
3 | cvv 3444 | . . 3 class V | |
4 | vf | . . . . . . 7 setvar π | |
5 | 4 | cv 1541 | . . . . . 6 class π |
6 | vp | . . . . . . 7 setvar π | |
7 | 6 | cv 1541 | . . . . . 6 class π |
8 | 2 | cv 1541 | . . . . . . 7 class π |
9 | cpths 28702 | . . . . . . 7 class Paths | |
10 | 8, 9 | cfv 6497 | . . . . . 6 class (Pathsβπ) |
11 | 5, 7, 10 | wbr 5106 | . . . . 5 wff π(Pathsβπ)π |
12 | cc0 11056 | . . . . . . 7 class 0 | |
13 | 12, 7 | cfv 6497 | . . . . . 6 class (πβ0) |
14 | chash 14236 | . . . . . . . 8 class β― | |
15 | 5, 14 | cfv 6497 | . . . . . . 7 class (β―βπ) |
16 | 15, 7 | cfv 6497 | . . . . . 6 class (πβ(β―βπ)) |
17 | 13, 16 | wceq 1542 | . . . . 5 wff (πβ0) = (πβ(β―βπ)) |
18 | 11, 17 | wa 397 | . . . 4 wff (π(Pathsβπ)π β§ (πβ0) = (πβ(β―βπ))) |
19 | 18, 4, 6 | copab 5168 | . . 3 class {β¨π, πβ© β£ (π(Pathsβπ)π β§ (πβ0) = (πβ(β―βπ)))} |
20 | 2, 3, 19 | cmpt 5189 | . 2 class (π β V β¦ {β¨π, πβ© β£ (π(Pathsβπ)π β§ (πβ0) = (πβ(β―βπ)))}) |
21 | 1, 20 | wceq 1542 | 1 wff Cycles = (π β V β¦ {β¨π, πβ© β£ (π(Pathsβπ)π β§ (πβ0) = (πβ(β―βπ)))}) |
Colors of variables: wff setvar class |
This definition is referenced by: cycls 28779 acycgr0v 33799 prclisacycgr 33802 |
Copyright terms: Public domain | W3C validator |