![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-crcts | Structured version Visualization version GIF version |
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 |
---|---|
df-crcts | β’ Circuits = (π β V β¦ {β¨π, πβ© β£ (π(Trailsβπ)π β§ (πβ0) = (πβ(β―βπ)))}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ccrcts 28774 | . 2 class Circuits | |
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 | ctrls 28680 | . . . . . . 7 class Trails | |
10 | 8, 9 | cfv 6497 | . . . . . 6 class (Trailsβπ) |
11 | 5, 7, 10 | wbr 5106 | . . . . 5 wff π(Trailsβπ)π |
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 (π(Trailsβπ)π β§ (πβ0) = (πβ(β―βπ))) |
19 | 18, 4, 6 | copab 5168 | . . 3 class {β¨π, πβ© β£ (π(Trailsβπ)π β§ (πβ0) = (πβ(β―βπ)))} |
20 | 2, 3, 19 | cmpt 5189 | . 2 class (π β V β¦ {β¨π, πβ© β£ (π(Trailsβπ)π β§ (πβ0) = (πβ(β―βπ)))}) |
21 | 1, 20 | wceq 1542 | 1 wff Circuits = (π β V β¦ {β¨π, πβ© β£ (π(Trailsβπ)π β§ (πβ0) = (πβ(β―βπ)))}) |
Colors of variables: wff setvar class |
This definition is referenced by: crcts 28778 |
Copyright terms: Public domain | W3C validator |