Definition df-crcts

Description: Define the set of all circuits (in an undirected graph).

According to Wikipedia ("Cycle (graph theory)", https://en.wikipedia.org/wiki/Cycle_(graph_theory) , 3-Oct-2017): "A circuit can be a closed walk allowing repetitions of vertices but not edges"; according to Wikipedia ("Glossary of graph theory terms", https://en.wikipedia.org/wiki/Glossary_of_graph_theory_terms, 3-Oct-2017): "A circuit may refer to ... a trail (a closed tour without repeated edges), ...".

Following Bollobas ("A trail whose endvertices coincide (a closed trail) is called a circuit.", see Definition of Bollobas p. 5.), a circuit is a closed trail without repeated edges. So the circuit is also represented by the following sequence: p(0) e(f(1)) p(1) e(f(2)) ... 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-crcts	|- Circuits = ( g e. _V |-> { <. f , p >. | ( f ( Trails ` g ) p /\ ( p ` 0 ) = ( p ` ( # ` f ) ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccrcts	|- Circuits
1		vg	|- g
2		cvv	|- _V
3		vf	|- f
4		vp	|- p
5	3	cv	|- f
6		ctrls	|- Trails
7	1	cv	|- g
8	7 6	cfv	|- ( Trails ` g )
9	4	cv	|- p
10	5 9 8	wbr	|- f ( Trails ` g ) p
11		cc0	|- 0
12	11 9	cfv	|- ( p ` 0 )
13		chash	|- #
14	5 13	cfv	|- ( # ` f )
15	14 9	cfv	|- ( p ` ( # ` f ) )
16	12 15	wceq	|- ( p ` 0 ) = ( p ` ( # ` f ) )
17	10 16	wa	|- ( f ( Trails ` g ) p /\ ( p ` 0 ) = ( p ` ( # ` f ) ) )
18	17 3 4	copab	|- { <. f , p >. | ( f ( Trails ` g ) p /\ ( p ` 0 ) = ( p ` ( # ` f ) ) ) }
19	1 2 18	cmpt	|- ( g e. _V |-> { <. f , p >. | ( f ( Trails ` g ) p /\ ( p ` 0 ) = ( p ` ( # ` f ) ) ) } )
20	0 19	wceq	|- Circuits = ( g e. _V |-> { <. f , p >. | ( f ( Trails ` g ) p /\ ( p ` 0 ) = ( p ` ( # ` f ) ) ) } )