![]() |
Metamath
Proof Explorer Theorem List (p. 296 of 481) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30640) |
![]() (30641-32163) |
![]() (32164-48040) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | clwlkwlk 29501 | Closed walks are walks (in an undirected graph). (Contributed by Alexander van der Vekens, 23-Jun-2018.) (Revised by AV, 16-Feb-2021.) (Proof shortened by AV, 30-Oct-2021.) |
β’ (π β (ClWalksβπΊ) β π β (WalksβπΊ)) | ||
Theorem | clwlkswks 29502 | Closed walks are walks (in an undirected graph). (Contributed by Alexander van der Vekens, 25-Aug-2018.) (Revised by AV, 16-Feb-2021.) |
β’ (ClWalksβπΊ) β (WalksβπΊ) | ||
Theorem | isclwlke 29503* | Properties of a pair of functions to be a closed walk (in an undirected graph). (Contributed by Alexander van der Vekens, 24-Jun-2018.) (Revised by AV, 16-Feb-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) β β’ (πΊ β π β (πΉ(ClWalksβπΊ)π β ((πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆπ) β§ (βπ β (0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ))) β§ (πβ0) = (πβ(β―βπΉ)))))) | ||
Theorem | isclwlkupgr 29504* | Properties of a pair of functions to be a closed walk (in a pseudograph). (Contributed by Alexander van der Vekens, 24-Jun-2018.) (Revised by AV, 11-Apr-2021.) (Revised by AV, 28-Oct-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) β β’ (πΊ β UPGraph β (πΉ(ClWalksβπΊ)π β ((πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆπ) β§ (βπ β (0..^(β―βπΉ))(πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))} β§ (πβ0) = (πβ(β―βπΉ)))))) | ||
Theorem | clwlkcomp 29505* | A closed walk expressed by properties of its components. (Contributed by Alexander van der Vekens, 24-Jun-2018.) (Revised by AV, 17-Feb-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ πΉ = (1st βπ) & β’ π = (2nd βπ) β β’ ((πΊ β π β§ π β (π Γ π)) β (π β (ClWalksβπΊ) β ((πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆπ) β§ (βπ β (0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ))) β§ (πβ0) = (πβ(β―βπΉ)))))) | ||
Theorem | clwlkcompim 29506* | Implications for the properties of the components of a closed walk. (Contributed by Alexander van der Vekens, 24-Jun-2018.) (Revised by AV, 17-Feb-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ πΉ = (1st βπ) & β’ π = (2nd βπ) β β’ (π β (ClWalksβπΊ) β ((πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆπ) β§ (βπ β (0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ))) β§ (πβ0) = (πβ(β―βπΉ))))) | ||
Theorem | upgrclwlkcompim 29507* | Implications for the properties of the components of a closed walk in a pseudograph. (Contributed by Alexander van der Vekens, 24-Jun-2018.) (Revised by AV, 2-May-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ πΉ = (1st βπ) & β’ π = (2nd βπ) β β’ ((πΊ β UPGraph β§ π β (ClWalksβπΊ)) β ((πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆπ) β§ βπ β (0..^(β―βπΉ))(πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))} β§ (πβ0) = (πβ(β―βπΉ)))) | ||
Theorem | clwlkcompbp 29508 | Basic properties of the components of a closed walk. (Contributed by AV, 23-May-2022.) |
β’ πΉ = (1st βπ) & β’ π = (2nd βπ) β β’ (π β (ClWalksβπΊ) β (πΉ(WalksβπΊ)π β§ (πβ0) = (πβ(β―βπΉ)))) | ||
Theorem | clwlkl1loop 29509 | A closed walk of length 1 is a loop. (Contributed by AV, 22-Apr-2021.) |
β’ ((Fun (iEdgβπΊ) β§ πΉ(ClWalksβπΊ)π β§ (β―βπΉ) = 1) β ((πβ0) = (πβ1) β§ {(πβ0)} β (EdgβπΊ))) | ||
Syntax | ccrcts 29510 | Extend class notation with circuits (in a graph). |
class Circuits | ||
Syntax | ccycls 29511 | Extend class notation with cycles (in a graph). |
class Cycles | ||
Definition | df-crcts 29512* |
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.) |
β’ Circuits = (π β V β¦ {β¨π, πβ© β£ (π(Trailsβπ)π β§ (πβ0) = (πβ(β―βπ)))}) | ||
Definition | df-cycls 29513* |
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.) |
β’ Cycles = (π β V β¦ {β¨π, πβ© β£ (π(Pathsβπ)π β§ (πβ0) = (πβ(β―βπ)))}) | ||
Theorem | crcts 29514* | The set of circuits (in an undirected graph). (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.) |
β’ (CircuitsβπΊ) = {β¨π, πβ© β£ (π(TrailsβπΊ)π β§ (πβ0) = (πβ(β―βπ)))} | ||
Theorem | cycls 29515* | The set of cycles (in an undirected graph). (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.) |
β’ (CyclesβπΊ) = {β¨π, πβ© β£ (π(PathsβπΊ)π β§ (πβ0) = (πβ(β―βπ)))} | ||
Theorem | iscrct 29516 | Sufficient and necessary conditions for a pair of functions to be a circuit (in an undirected graph): A pair of function "is" (represents) a circuit iff it is a closed trail. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.) (Revised by AV, 30-Oct-2021.) |
β’ (πΉ(CircuitsβπΊ)π β (πΉ(TrailsβπΊ)π β§ (πβ0) = (πβ(β―βπΉ)))) | ||
Theorem | iscycl 29517 | Sufficient and necessary conditions for a pair of functions to be a cycle (in an undirected graph): A pair of function "is" (represents) a cycle iff it is a closed path. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.) (Revised by AV, 30-Oct-2021.) |
β’ (πΉ(CyclesβπΊ)π β (πΉ(PathsβπΊ)π β§ (πβ0) = (πβ(β―βπΉ)))) | ||
Theorem | crctprop 29518 | The properties of a circuit: A circuit is a closed trail. (Contributed by AV, 31-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.) |
β’ (πΉ(CircuitsβπΊ)π β (πΉ(TrailsβπΊ)π β§ (πβ0) = (πβ(β―βπΉ)))) | ||
Theorem | cyclprop 29519 | The properties of a cycle: A cycle is a closed path. (Contributed by AV, 31-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.) |
β’ (πΉ(CyclesβπΊ)π β (πΉ(PathsβπΊ)π β§ (πβ0) = (πβ(β―βπΉ)))) | ||
Theorem | crctisclwlk 29520 | A circuit is a closed walk. (Contributed by AV, 17-Feb-2021.) (Proof shortened by AV, 30-Oct-2021.) |
β’ (πΉ(CircuitsβπΊ)π β πΉ(ClWalksβπΊ)π) | ||
Theorem | crctistrl 29521 | A circuit is a trail. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.) |
β’ (πΉ(CircuitsβπΊ)π β πΉ(TrailsβπΊ)π) | ||
Theorem | crctiswlk 29522 | A circuit is a walk. (Contributed by AV, 6-Apr-2021.) |
β’ (πΉ(CircuitsβπΊ)π β πΉ(WalksβπΊ)π) | ||
Theorem | cyclispth 29523 | A cycle is a path. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.) |
β’ (πΉ(CyclesβπΊ)π β πΉ(PathsβπΊ)π) | ||
Theorem | cycliswlk 29524 | A cycle is a walk. (Contributed by Alexander van der Vekens, 7-Nov-2017.) (Revised by AV, 31-Jan-2021.) |
β’ (πΉ(CyclesβπΊ)π β πΉ(WalksβπΊ)π) | ||
Theorem | cycliscrct 29525 | A cycle is a circuit. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.) |
β’ (πΉ(CyclesβπΊ)π β πΉ(CircuitsβπΊ)π) | ||
Theorem | cyclnspth 29526 | A (non-trivial) cycle is not a simple path. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.) |
β’ (πΉ β β β (πΉ(CyclesβπΊ)π β Β¬ πΉ(SPathsβπΊ)π)) | ||
Theorem | cyclispthon 29527 | A cycle is a path starting and ending at its first vertex. (Contributed by Alexander van der Vekens, 8-Nov-2017.) (Revised by AV, 31-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.) |
β’ (πΉ(CyclesβπΊ)π β πΉ((πβ0)(PathsOnβπΊ)(πβ0))π) | ||
Theorem | lfgrn1cycl 29528* | In a loop-free graph there are no cycles with length 1 (consisting of one edge). (Contributed by Alexander van der Vekens, 7-Nov-2017.) (Revised by AV, 2-Feb-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) β β’ (πΌ:dom πΌβΆ{π₯ β π« π β£ 2 β€ (β―βπ₯)} β (πΉ(CyclesβπΊ)π β (β―βπΉ) β 1)) | ||
Theorem | usgr2trlncrct 29529 | In a simple graph, any trail of length 2 is not a circuit. (Contributed by AV, 5-Jun-2021.) |
β’ ((πΊ β USGraph β§ (β―βπΉ) = 2) β (πΉ(TrailsβπΊ)π β Β¬ πΉ(CircuitsβπΊ)π)) | ||
Theorem | umgrn1cycl 29530 | In a multigraph graph (with no loops!) there are no cycles with length 1 (consisting of one edge). (Contributed by Alexander van der Vekens, 7-Nov-2017.) (Revised by AV, 2-Feb-2021.) |
β’ ((πΊ β UMGraph β§ πΉ(CyclesβπΊ)π) β (β―βπΉ) β 1) | ||
Theorem | uspgrn2crct 29531 | In a simple pseudograph there are no circuits with length 2 (consisting of two edges). (Contributed by Alexander van der Vekens, 9-Nov-2017.) (Revised by AV, 3-Feb-2021.) (Proof shortened by AV, 31-Oct-2021.) |
β’ ((πΊ β USPGraph β§ πΉ(CircuitsβπΊ)π) β (β―βπΉ) β 2) | ||
Theorem | usgrn2cycl 29532 | In a simple graph there are no cycles with length 2 (consisting of two edges). (Contributed by Alexander van der Vekens, 9-Nov-2017.) (Revised by AV, 4-Feb-2021.) |
β’ ((πΊ β USGraph β§ πΉ(CyclesβπΊ)π) β (β―βπΉ) β 2) | ||
Theorem | crctcshwlkn0lem1 29533 | Lemma for crctcshwlkn0 29544. (Contributed by AV, 13-Mar-2021.) |
β’ ((π΄ β β β§ π΅ β β) β ((π΄ β π΅) + 1) β€ π΄) | ||
Theorem | crctcshwlkn0lem2 29534* | Lemma for crctcshwlkn0 29544. (Contributed by AV, 12-Mar-2021.) |
β’ (π β π β (1..^π)) & β’ π = (π₯ β (0...π) β¦ if(π₯ β€ (π β π), (πβ(π₯ + π)), (πβ((π₯ + π) β π)))) β β’ ((π β§ π½ β (0...(π β π))) β (πβπ½) = (πβ(π½ + π))) | ||
Theorem | crctcshwlkn0lem3 29535* | Lemma for crctcshwlkn0 29544. (Contributed by AV, 12-Mar-2021.) |
β’ (π β π β (1..^π)) & β’ π = (π₯ β (0...π) β¦ if(π₯ β€ (π β π), (πβ(π₯ + π)), (πβ((π₯ + π) β π)))) β β’ ((π β§ π½ β (((π β π) + 1)...π)) β (πβπ½) = (πβ((π½ + π) β π))) | ||
Theorem | crctcshwlkn0lem4 29536* | Lemma for crctcshwlkn0 29544. (Contributed by AV, 12-Mar-2021.) |
β’ (π β π β (1..^π)) & β’ π = (π₯ β (0...π) β¦ if(π₯ β€ (π β π), (πβ(π₯ + π)), (πβ((π₯ + π) β π)))) & β’ π» = (πΉ cyclShift π) & β’ π = (β―βπΉ) & β’ (π β πΉ β Word π΄) & β’ (π β βπ β (0..^π)if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ)))) β β’ (π β βπ β (0..^(π β π))if-((πβπ) = (πβ(π + 1)), (πΌβ(π»βπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(π»βπ)))) | ||
Theorem | crctcshwlkn0lem5 29537* | Lemma for crctcshwlkn0 29544. (Contributed by AV, 12-Mar-2021.) |
β’ (π β π β (1..^π)) & β’ π = (π₯ β (0...π) β¦ if(π₯ β€ (π β π), (πβ(π₯ + π)), (πβ((π₯ + π) β π)))) & β’ π» = (πΉ cyclShift π) & β’ π = (β―βπΉ) & β’ (π β πΉ β Word π΄) & β’ (π β βπ β (0..^π)if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ)))) β β’ (π β βπ β (((π β π) + 1)..^π)if-((πβπ) = (πβ(π + 1)), (πΌβ(π»βπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(π»βπ)))) | ||
Theorem | crctcshwlkn0lem6 29538* | Lemma for crctcshwlkn0 29544. (Contributed by AV, 12-Mar-2021.) |
β’ (π β π β (1..^π)) & β’ π = (π₯ β (0...π) β¦ if(π₯ β€ (π β π), (πβ(π₯ + π)), (πβ((π₯ + π) β π)))) & β’ π» = (πΉ cyclShift π) & β’ π = (β―βπΉ) & β’ (π β πΉ β Word π΄) & β’ (π β βπ β (0..^π)if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ)))) & β’ (π β (πβπ) = (πβ0)) β β’ ((π β§ π½ = (π β π)) β if-((πβπ½) = (πβ(π½ + 1)), (πΌβ(π»βπ½)) = {(πβπ½)}, {(πβπ½), (πβ(π½ + 1))} β (πΌβ(π»βπ½)))) | ||
Theorem | crctcshwlkn0lem7 29539* | Lemma for crctcshwlkn0 29544. (Contributed by AV, 12-Mar-2021.) |
β’ (π β π β (1..^π)) & β’ π = (π₯ β (0...π) β¦ if(π₯ β€ (π β π), (πβ(π₯ + π)), (πβ((π₯ + π) β π)))) & β’ π» = (πΉ cyclShift π) & β’ π = (β―βπΉ) & β’ (π β πΉ β Word π΄) & β’ (π β βπ β (0..^π)if-((πβπ) = (πβ(π + 1)), (πΌβ(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(πΉβπ)))) & β’ (π β (πβπ) = (πβ0)) β β’ (π β βπ β (0..^π)if-((πβπ) = (πβ(π + 1)), (πΌβ(π»βπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β (πΌβ(π»βπ)))) | ||
Theorem | crctcshlem1 29540 | Lemma for crctcsh 29547. (Contributed by AV, 10-Mar-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β πΉ(CircuitsβπΊ)π) & β’ π = (β―βπΉ) β β’ (π β π β β0) | ||
Theorem | crctcshlem2 29541 | Lemma for crctcsh 29547. (Contributed by AV, 10-Mar-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β πΉ(CircuitsβπΊ)π) & β’ π = (β―βπΉ) & β’ (π β π β (0..^π)) & β’ π» = (πΉ cyclShift π) β β’ (π β (β―βπ») = π) | ||
Theorem | crctcshlem3 29542* | Lemma for crctcsh 29547. (Contributed by AV, 10-Mar-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β πΉ(CircuitsβπΊ)π) & β’ π = (β―βπΉ) & β’ (π β π β (0..^π)) & β’ π» = (πΉ cyclShift π) & β’ π = (π₯ β (0...π) β¦ if(π₯ β€ (π β π), (πβ(π₯ + π)), (πβ((π₯ + π) β π)))) β β’ (π β (πΊ β V β§ π» β V β§ π β V)) | ||
Theorem | crctcshlem4 29543* | Lemma for crctcsh 29547. (Contributed by AV, 10-Mar-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β πΉ(CircuitsβπΊ)π) & β’ π = (β―βπΉ) & β’ (π β π β (0..^π)) & β’ π» = (πΉ cyclShift π) & β’ π = (π₯ β (0...π) β¦ if(π₯ β€ (π β π), (πβ(π₯ + π)), (πβ((π₯ + π) β π)))) β β’ ((π β§ π = 0) β (π» = πΉ β§ π = π)) | ||
Theorem | crctcshwlkn0 29544* | Cyclically shifting the indices of a circuit β¨πΉ, πβ© results in a walk β¨π», πβ©. (Contributed by AV, 10-Mar-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β πΉ(CircuitsβπΊ)π) & β’ π = (β―βπΉ) & β’ (π β π β (0..^π)) & β’ π» = (πΉ cyclShift π) & β’ π = (π₯ β (0...π) β¦ if(π₯ β€ (π β π), (πβ(π₯ + π)), (πβ((π₯ + π) β π)))) β β’ ((π β§ π β 0) β π»(WalksβπΊ)π) | ||
Theorem | crctcshwlk 29545* | Cyclically shifting the indices of a circuit β¨πΉ, πβ© results in a walk β¨π», πβ©. (Contributed by AV, 10-Mar-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β πΉ(CircuitsβπΊ)π) & β’ π = (β―βπΉ) & β’ (π β π β (0..^π)) & β’ π» = (πΉ cyclShift π) & β’ π = (π₯ β (0...π) β¦ if(π₯ β€ (π β π), (πβ(π₯ + π)), (πβ((π₯ + π) β π)))) β β’ (π β π»(WalksβπΊ)π) | ||
Theorem | crctcshtrl 29546* | Cyclically shifting the indices of a circuit β¨πΉ, πβ© results in a trail β¨π», πβ©. (Contributed by AV, 14-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β πΉ(CircuitsβπΊ)π) & β’ π = (β―βπΉ) & β’ (π β π β (0..^π)) & β’ π» = (πΉ cyclShift π) & β’ π = (π₯ β (0...π) β¦ if(π₯ β€ (π β π), (πβ(π₯ + π)), (πβ((π₯ + π) β π)))) β β’ (π β π»(TrailsβπΊ)π) | ||
Theorem | crctcsh 29547* | Cyclically shifting the indices of a circuit β¨πΉ, πβ© results in a circuit β¨π», πβ©. (Contributed by AV, 10-Mar-2021.) (Proof shortened by AV, 31-Oct-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) & β’ (π β πΉ(CircuitsβπΊ)π) & β’ π = (β―βπΉ) & β’ (π β π β (0..^π)) & β’ π» = (πΉ cyclShift π) & β’ π = (π₯ β (0...π) β¦ if(π₯ β€ (π β π), (πβ(π₯ + π)), (πβ((π₯ + π) β π)))) β β’ (π β π»(CircuitsβπΊ)π) | ||
In general, a walk is an alternating sequence of vertices and edges, as defined in df-wlks 29325: p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n). Often, it is sufficient to refer to a walk by the natural sequence of its vertices, i.e omitting its edges in its representation: p(0) p(1) ... p(n-1) p(n), see the corresponding remark in [Diestel] p. 6. The concept of a Word, see df-word 14462, is the appropriate way to define such a sequence (being finite and starting at index 0) of vertices. Therefore, it is used in Definitions df-wwlks 29553 and df-wwlksn 29554, and the representation of a walk as sequence of its vertices is called "walk as word". Only for simple pseudographs, however, the edges can be uniquely reconstructed from such a representation. In other cases, there could be more than one edge between two adjacent vertices in the walk (in a multigraph), or two adjacent vertices could be connected by two different hyperedges involving additional vertices (in a hypergraph). | ||
Syntax | cwwlks 29548 | Extend class notation with walks (in a graph) as word over the set of vertices. |
class WWalks | ||
Syntax | cwwlksn 29549 | Extend class notation with walks (in a graph) of a fixed length as word over the set of vertices. |
class WWalksN | ||
Syntax | cwwlksnon 29550 | Extend class notation with walks between two vertices (in a graph) of a fixed length as word over the set of vertices. |
class WWalksNOn | ||
Syntax | cwwspthsn 29551 | Extend class notation with simple paths (in a graph) of a fixed length as word over the set of vertices. |
class WSPathsN | ||
Syntax | cwwspthsnon 29552 | Extend class notation with simple paths between two vertices (in a graph) of a fixed length as word over the set of vertices. |
class WSPathsNOn | ||
Definition | df-wwlks 29553* | Define the set of all walks (in an undirected graph) as words over the set of vertices. Such a word corresponds to the sequence p(0) p(1) ... p(n-1) p(n) of the vertices in a walk p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n) as defined in df-wlks 29325. π€ = β has to be excluded because a walk always consists of at least one vertex, see wlkn0 29347. (Contributed by Alexander van der Vekens, 15-Jul-2018.) (Revised by AV, 8-Apr-2021.) |
β’ WWalks = (π β V β¦ {π€ β Word (Vtxβπ) β£ (π€ β β β§ βπ β (0..^((β―βπ€) β 1)){(π€βπ), (π€β(π + 1))} β (Edgβπ))}) | ||
Definition | df-wwlksn 29554* | Define the set of all walks (in an undirected graph) of a fixed length n as words over the set of vertices. Such a word corresponds to the sequence p(0) p(1) ... p(n) of the vertices in a walk p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n) as defined in df-wlks 29325. (Contributed by Alexander van der Vekens, 15-Jul-2018.) (Revised by AV, 8-Apr-2021.) |
β’ WWalksN = (π β β0, π β V β¦ {π€ β (WWalksβπ) β£ (β―βπ€) = (π + 1)}) | ||
Definition | df-wwlksnon 29555* | Define the collection of walks of a fixed length with particular endpoints as word over the set of vertices. (Contributed by Alexander van der Vekens, 15-Feb-2018.) (Revised by AV, 11-May-2021.) |
β’ WWalksNOn = (π β β0, π β V β¦ (π β (Vtxβπ), π β (Vtxβπ) β¦ {π€ β (π WWalksN π) β£ ((π€β0) = π β§ (π€βπ) = π)})) | ||
Definition | df-wspthsn 29556* | Define the collection of simple paths of a fixed length as word over the set of vertices. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 11-May-2021.) |
β’ WSPathsN = (π β β0, π β V β¦ {π€ β (π WWalksN π) β£ βπ π(SPathsβπ)π€}) | ||
Definition | df-wspthsnon 29557* | Define the collection of simple paths of a fixed length with particular endpoints as word over the set of vertices. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 11-May-2021.) |
β’ WSPathsNOn = (π β β0, π β V β¦ (π β (Vtxβπ), π β (Vtxβπ) β¦ {π€ β (π(π WWalksNOn π)π) β£ βπ π(π(SPathsOnβπ)π)π€})) | ||
Theorem | wwlks 29558* | The set of walks (in an undirected graph) as words over the set of vertices. (Contributed by Alexander van der Vekens, 15-Jul-2018.) (Revised by AV, 8-Apr-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ (WWalksβπΊ) = {π€ β Word π β£ (π€ β β β§ βπ β (0..^((β―βπ€) β 1)){(π€βπ), (π€β(π + 1))} β πΈ)} | ||
Theorem | iswwlks 29559* | A word over the set of vertices representing a walk (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Jul-2018.) (Revised by AV, 8-Apr-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ (π β (WWalksβπΊ) β (π β β β§ π β Word π β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β πΈ)) | ||
Theorem | wwlksn 29560* | The set of walks (in an undirected graph) of a fixed length as words over the set of vertices. (Contributed by Alexander van der Vekens, 15-Jul-2018.) (Revised by AV, 8-Apr-2021.) |
β’ (π β β0 β (π WWalksN πΊ) = {π€ β (WWalksβπΊ) β£ (β―βπ€) = (π + 1)}) | ||
Theorem | iswwlksn 29561 | A word over the set of vertices representing a walk of a fixed length (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Jul-2018.) (Revised by AV, 8-Apr-2021.) |
β’ (π β β0 β (π β (π WWalksN πΊ) β (π β (WWalksβπΊ) β§ (β―βπ) = (π + 1)))) | ||
Theorem | wwlksnprcl 29562 | Derivation of the length of a word π whose concatenation with a singleton word represents a walk of a fixed length π (a partial reverse closure theorem). (Contributed by AV, 4-Mar-2022.) |
β’ ((π β Word π β§ π β β0) β ((π ++ β¨βπββ©) β (π WWalksN πΊ) β (β―βπ) = π)) | ||
Theorem | iswwlksnx 29563* | Properties of a word to represent a walk of a fixed length, definition of WWalks expanded. (Contributed by AV, 28-Apr-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ (π β β0 β (π β (π WWalksN πΊ) β (π β Word π β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β πΈ β§ (β―βπ) = (π + 1)))) | ||
Theorem | wwlkbp 29564 | Basic properties of a walk (in an undirected graph) as word. (Contributed by Alexander van der Vekens, 15-Jul-2018.) (Revised by AV, 9-Apr-2021.) |
β’ π = (VtxβπΊ) β β’ (π β (WWalksβπΊ) β (πΊ β V β§ π β Word π)) | ||
Theorem | wwlknbp 29565 | Basic properties of a walk of a fixed length (in an undirected graph) as word. (Contributed by Alexander van der Vekens, 16-Jul-2018.) (Revised by AV, 9-Apr-2021.) (Proof shortened by AV, 20-May-2021.) |
β’ π = (VtxβπΊ) β β’ (π β (π WWalksN πΊ) β (πΊ β V β§ π β β0 β§ π β Word π)) | ||
Theorem | wwlknp 29566* | Properties of a set being a walk of length n (represented by a word). (Contributed by Alexander van der Vekens, 17-Jun-2018.) (Revised by AV, 9-Apr-2021.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) β β’ (π β (π WWalksN πΊ) β (π β Word π β§ (β―βπ) = (π + 1) β§ βπ β (0..^π){(πβπ), (πβ(π + 1))} β πΈ)) | ||
Theorem | wwlknbp1 29567 | Other basic properties of a walk of a fixed length as word. (Contributed by AV, 8-Mar-2022.) |
β’ (π β (π WWalksN πΊ) β (π β β0 β§ π β Word (VtxβπΊ) β§ (β―βπ) = (π + 1))) | ||
Theorem | wwlknvtx 29568* | The symbols of a word π representing a walk of a fixed length π are vertices. (Contributed by AV, 16-Mar-2022.) |
β’ (π β (π WWalksN πΊ) β βπ β (0...π)(πβπ) β (VtxβπΊ)) | ||
Theorem | wwlknllvtx 29569 | If a word π represents a walk of a fixed length π, then the first and the last symbol of the word is a vertex. (Contributed by AV, 14-Mar-2022.) |
β’ π = (VtxβπΊ) β β’ (π β (π WWalksN πΊ) β ((πβ0) β π β§ (πβπ) β π)) | ||
Theorem | wwlknlsw 29570 | If a word represents a walk of a fixed length, then the last symbol of the word is the endvertex of the walk. (Contributed by AV, 8-Mar-2022.) |
β’ (π β (π WWalksN πΊ) β (πβπ) = (lastSβπ)) | ||
Theorem | wspthsn 29571* | The set of simple paths of a fixed length as word. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 11-May-2021.) |
β’ (π WSPathsN πΊ) = {π€ β (π WWalksN πΊ) β£ βπ π(SPathsβπΊ)π€} | ||
Theorem | iswspthn 29572* | An element of the set of simple paths of a fixed length as word. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 11-May-2021.) |
β’ (π β (π WSPathsN πΊ) β (π β (π WWalksN πΊ) β§ βπ π(SPathsβπΊ)π)) | ||
Theorem | wspthnp 29573* | Properties of a set being a simple path of a fixed length as word. (Contributed by AV, 18-May-2021.) |
β’ (π β (π WSPathsN πΊ) β ((π β β0 β§ πΊ β V) β§ π β (π WWalksN πΊ) β§ βπ π(SPathsβπΊ)π)) | ||
Theorem | wwlksnon 29574* | The set of walks of a fixed length between two vertices as word. (Contributed by Alexander van der Vekens, 15-Feb-2018.) (Revised by AV, 11-May-2021.) |
β’ π = (VtxβπΊ) β β’ ((π β β0 β§ πΊ β π) β (π WWalksNOn πΊ) = (π β π, π β π β¦ {π€ β (π WWalksN πΊ) β£ ((π€β0) = π β§ (π€βπ) = π)})) | ||
Theorem | wspthsnon 29575* | The set of simple paths of a fixed length between two vertices as word. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 11-May-2021.) |
β’ π = (VtxβπΊ) β β’ ((π β β0 β§ πΊ β π) β (π WSPathsNOn πΊ) = (π β π, π β π β¦ {π€ β (π(π WWalksNOn πΊ)π) β£ βπ π(π(SPathsOnβπΊ)π)π€})) | ||
Theorem | iswwlksnon 29576* | The set of walks of a fixed length between two vertices as word. (Contributed by Alexander van der Vekens, 15-Feb-2018.) (Revised by AV, 12-May-2021.) (Revised by AV, 14-Mar-2022.) |
β’ π = (VtxβπΊ) β β’ (π΄(π WWalksNOn πΊ)π΅) = {π€ β (π WWalksN πΊ) β£ ((π€β0) = π΄ β§ (π€βπ) = π΅)} | ||
Theorem | wwlksnon0 29577 | Sufficient conditions for a set of walks of a fixed length between two vertices to be empty. (Contributed by AV, 15-May-2021.) (Proof shortened by AV, 21-May-2021.) |
β’ π = (VtxβπΊ) β β’ (Β¬ ((π β β0 β§ πΊ β V) β§ (π΄ β π β§ π΅ β π)) β (π΄(π WWalksNOn πΊ)π΅) = β ) | ||
Theorem | wwlksonvtx 29578 | If a word π represents a walk of length 2 on two classes π΄ and πΆ, these classes are vertices. (Contributed by AV, 14-Mar-2022.) |
β’ π = (VtxβπΊ) β β’ (π β (π΄(π WWalksNOn πΊ)πΆ) β (π΄ β π β§ πΆ β π)) | ||
Theorem | iswspthsnon 29579* | The set of simple paths of a fixed length between two vertices as word. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 12-May-2021.) (Revised by AV, 14-Mar-2022.) |
β’ π = (VtxβπΊ) β β’ (π΄(π WSPathsNOn πΊ)π΅) = {π€ β (π΄(π WWalksNOn πΊ)π΅) β£ βπ π(π΄(SPathsOnβπΊ)π΅)π€} | ||
Theorem | wwlknon 29580 | An element of the set of walks of a fixed length between two vertices as word. (Contributed by Alexander van der Vekens, 15-Feb-2018.) (Revised by AV, 12-May-2021.) (Revised by AV, 14-Mar-2022.) |
β’ (π β (π΄(π WWalksNOn πΊ)π΅) β (π β (π WWalksN πΊ) β§ (πβ0) = π΄ β§ (πβπ) = π΅)) | ||
Theorem | wspthnon 29581* | An element of the set of simple paths of a fixed length between two vertices as word. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 12-May-2021.) (Revised by AV, 15-Mar-2022.) |
β’ (π β (π΄(π WSPathsNOn πΊ)π΅) β (π β (π΄(π WWalksNOn πΊ)π΅) β§ βπ π(π΄(SPathsOnβπΊ)π΅)π)) | ||
Theorem | wspthnonp 29582* | Properties of a set being a simple path of a fixed length between two vertices as word. (Contributed by AV, 14-May-2021.) (Proof shortened by AV, 15-Mar-2022.) |
β’ π = (VtxβπΊ) β β’ (π β (π΄(π WSPathsNOn πΊ)π΅) β ((π β β0 β§ πΊ β V) β§ (π΄ β π β§ π΅ β π) β§ (π β (π΄(π WWalksNOn πΊ)π΅) β§ βπ π(π΄(SPathsOnβπΊ)π΅)π))) | ||
Theorem | wspthneq1eq2 29583 | Two simple paths with identical sequences of vertices start and end at the same vertices. (Contributed by AV, 14-May-2021.) |
β’ ((π β (π΄(π WSPathsNOn πΊ)π΅) β§ π β (πΆ(π WSPathsNOn πΊ)π·)) β (π΄ = πΆ β§ π΅ = π·)) | ||
Theorem | wwlksn0s 29584* | The set of all walks as words of length 0 is the set of all words of length 1 over the vertices. (Contributed by Alexander van der Vekens, 22-Jul-2018.) (Revised by AV, 12-Apr-2021.) |
β’ (0 WWalksN πΊ) = {π€ β Word (VtxβπΊ) β£ (β―βπ€) = 1} | ||
Theorem | wwlkssswrd 29585 | Walks (represented by words) are words. (Contributed by Alexander van der Vekens, 17-Jul-2018.) (Revised by AV, 9-Apr-2021.) |
β’ π = (VtxβπΊ) β β’ (WWalksβπΊ) β Word π | ||
Theorem | wwlksn0 29586* | A walk of length 0 is represented by a singleton word. (Contributed by Alexander van der Vekens, 20-Jul-2018.) (Revised by AV, 9-Apr-2021.) (Proof shortened by AV, 21-May-2021.) |
β’ π = (VtxβπΊ) β β’ (π β (0 WWalksN πΊ) β βπ£ β π π = β¨βπ£ββ©) | ||
Theorem | 0enwwlksnge1 29587 | In graphs without edges, there are no walks of length greater than 0. (Contributed by Alexander van der Vekens, 26-Jul-2018.) (Revised by AV, 7-May-2021.) |
β’ (((EdgβπΊ) = β β§ π β β) β (π WWalksN πΊ) = β ) | ||
Theorem | wwlkswwlksn 29588 | A walk of a fixed length as word is a walk (in an undirected graph) as word. (Contributed by Alexander van der Vekens, 17-Jul-2018.) (Revised by AV, 12-Apr-2021.) |
β’ (π β (π WWalksN πΊ) β π β (WWalksβπΊ)) | ||
Theorem | wwlkssswwlksn 29589 | The walks of a fixed length as words are walks (in an undirected graph) as words. (Contributed by Alexander van der Vekens, 17-Jul-2018.) (Revised by AV, 12-Apr-2021.) |
β’ (π WWalksN πΊ) β (WWalksβπΊ) | ||
Theorem | wlkiswwlks1 29590 | The sequence of vertices in a walk is a walk as word in a pseudograph. (Contributed by Alexander van der Vekens, 20-Jul-2018.) (Revised by AV, 9-Apr-2021.) |
β’ (πΊ β UPGraph β (πΉ(WalksβπΊ)π β π β (WWalksβπΊ))) | ||
Theorem | wlklnwwlkln1 29591 | The sequence of vertices in a walk of length π is a walk as word of length π in a pseudograph. (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 12-Apr-2021.) |
β’ (πΊ β UPGraph β ((πΉ(WalksβπΊ)π β§ (β―βπΉ) = π) β π β (π WWalksN πΊ))) | ||
Theorem | wlkiswwlks2lem1 29592* | Lemma 1 for wlkiswwlks2 29598. (Contributed by Alexander van der Vekens, 20-Jul-2018.) |
β’ πΉ = (π₯ β (0..^((β―βπ) β 1)) β¦ (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))})) β β’ ((π β Word π β§ 1 β€ (β―βπ)) β (β―βπΉ) = ((β―βπ) β 1)) | ||
Theorem | wlkiswwlks2lem2 29593* | Lemma 2 for wlkiswwlks2 29598. (Contributed by Alexander van der Vekens, 20-Jul-2018.) |
β’ πΉ = (π₯ β (0..^((β―βπ) β 1)) β¦ (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))})) β β’ (((β―βπ) β β0 β§ πΌ β (0..^((β―βπ) β 1))) β (πΉβπΌ) = (β‘πΈβ{(πβπΌ), (πβ(πΌ + 1))})) | ||
Theorem | wlkiswwlks2lem3 29594* | Lemma 3 for wlkiswwlks2 29598. (Contributed by Alexander van der Vekens, 20-Jul-2018.) |
β’ πΉ = (π₯ β (0..^((β―βπ) β 1)) β¦ (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))})) β β’ ((π β Word π β§ 1 β€ (β―βπ)) β π:(0...(β―βπΉ))βΆπ) | ||
Theorem | wlkiswwlks2lem4 29595* | Lemma 4 for wlkiswwlks2 29598. (Contributed by Alexander van der Vekens, 20-Jul-2018.) (Revised by AV, 10-Apr-2021.) |
β’ πΉ = (π₯ β (0..^((β―βπ) β 1)) β¦ (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))})) & β’ πΈ = (iEdgβπΊ) β β’ ((πΊ β USPGraph β§ π β Word π β§ 1 β€ (β―βπ)) β (βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β βπ β (0..^(β―βπΉ))(πΈβ(πΉβπ)) = {(πβπ), (πβ(π + 1))})) | ||
Theorem | wlkiswwlks2lem5 29596* | Lemma 5 for wlkiswwlks2 29598. (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 10-Apr-2021.) |
β’ πΉ = (π₯ β (0..^((β―βπ) β 1)) β¦ (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))})) & β’ πΈ = (iEdgβπΊ) β β’ ((πΊ β USPGraph β§ π β Word π β§ 1 β€ (β―βπ)) β (βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β πΉ β Word dom πΈ)) | ||
Theorem | wlkiswwlks2lem6 29597* | Lemma 6 for wlkiswwlks2 29598. (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 10-Apr-2021.) |
β’ πΉ = (π₯ β (0..^((β―βπ) β 1)) β¦ (β‘πΈβ{(πβπ₯), (πβ(π₯ + 1))})) & β’ πΈ = (iEdgβπΊ) β β’ ((πΊ β USPGraph β§ π β Word π β§ 1 β€ (β―βπ)) β (βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β (πΉ β Word dom πΈ β§ π:(0...(β―βπΉ))βΆπ β§ βπ β (0..^(β―βπΉ))(πΈβ(πΉβπ)) = {(πβπ), (πβ(π + 1))}))) | ||
Theorem | wlkiswwlks2 29598* | A walk as word corresponds to the sequence of vertices in a walk in a simple pseudograph. (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 10-Apr-2021.) |
β’ (πΊ β USPGraph β (π β (WWalksβπΊ) β βπ π(WalksβπΊ)π)) | ||
Theorem | wlkiswwlks 29599* | A walk as word corresponds to a walk in a simple pseudograph. (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 10-Apr-2021.) |
β’ (πΊ β USPGraph β (βπ π(WalksβπΊ)π β π β (WWalksβπΊ))) | ||
Theorem | wlkiswwlksupgr2 29600* | A walk as word corresponds to the sequence of vertices in a walk in a pseudograph. This variant of wlkiswwlks2 29598 does not require πΊ to be a simple pseudograph, but it requires the Axiom of Choice (ac6 10471) for its proof. Notice that only the existence of a function π can be proven, but, in general, it cannot be "constructed" (as in wlkiswwlks2 29598). (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 10-Apr-2021.) |
β’ (πΊ β UPGraph β (π β (WWalksβπΊ) β βπ π(WalksβπΊ)π)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |