Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-crct Structured version   Unicode version

Definition df-crct 24188
 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.)
Assertion
Ref Expression
df-crct Circuits Trails
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-crct
StepHypRef Expression
1 ccrct 24182 . 2 Circuits
2 vv . . 3
3 ve . . 3
4 cvv 3113 . . 3
5 vf . . . . . . 7
65cv 1378 . . . . . 6
7 vp . . . . . . 7
87cv 1378 . . . . . 6
92cv 1378 . . . . . . 7
103cv 1378 . . . . . . 7
11 ctrail 24175 . . . . . . 7 Trails
129, 10, 11co 6282 . . . . . 6 Trails
136, 8, 12wbr 4447 . . . . 5 Trails
14 cc0 9488 . . . . . . 7
1514, 8cfv 5586 . . . . . 6
16 chash 12369 . . . . . . . 8
176, 16cfv 5586 . . . . . . 7
1817, 8cfv 5586 . . . . . 6
1915, 18wceq 1379 . . . . 5
2013, 19wa 369 . . . 4 Trails
2120, 5, 7copab 4504 . . 3 Trails
222, 3, 4, 4, 21cmpt2 6284 . 2 Trails
231, 22wceq 1379 1 Circuits Trails
 Colors of variables: wff setvar class This definition is referenced by:  crcts  24298  crctistrl  24304
 Copyright terms: Public domain W3C validator