df-cycls

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
	Assertion	df-cycls	$⊢ Cycles = (g \in V ⟼ \{⟨f, p⟩ \| (f Paths (g) p \land p (0) = p (\|f\|))\})$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccycls	$class Cycles$
1		vg	$setvar g$
2		cvv	$class V$
3		vf	$setvar f$
4		vp	$setvar p$
5	3	cv	$setvar f$
6		cpths	$class Paths$
7	1	cv	$setvar g$
8	7 6	cfv	$class Paths (g)$
9	4	cv	$setvar p$
10	5 9 8	wbr	$wff f Paths (g) p$
11		cc0	$class 0$
12	11 9	cfv	$class p (0)$
13		chash	$class \|.\|$
14	5 13	cfv	$class \|f\|$
15	14 9	cfv	$class p (\|f\|)$
16	12 15	wceq	$wff p (0) = p (\|f\|)$
17	10 16	wa	$wff (f Paths (g) p \land p (0) = p (\|f\|))$
18	17 3 4	copab	$class \{⟨f, p⟩ \| (f Paths (g) p \land p (0) = p (\|f\|))\}$
19	1 2 18	cmpt	$class (g \in V ⟼ \{⟨f, p⟩ \| (f Paths (g) p \land p (0) = p (\|f\|))\})$
20	0 19	wceq	$wff Cycles = (g \in V ⟼ \{⟨f, p⟩ \| (f Paths (g) p \land p (0) = p (\|f\|))\})$

Metamath Proof Explorer

Definition df-cycls

Detailed syntax breakdown