Metamath Proof Explorer


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 ) ) ) } )